diff --git a/src/bin/man/spot-x.x b/src/bin/man/spot-x.x index 631846215..af34ef95f 100644 --- a/src/bin/man/spot-x.x +++ b/src/bin/man/spot-x.x @@ -14,12 +14,13 @@ spot-x \- Common fine-tuning options. .TP \fBSPOT_SATSOLVER\fR If set, this variable should indicate how to call a SAT\-solver. This -is used by the sat\-minimize option described above. The default value -is \f(CW"glucose %I >%O"\fR. The escape sequences \f(CW%I\fR and \f(CW%O\fR -respectively denote the names of the input and output files. These -temporary files are created in the directory specified by \fBSPOT_TMPDIR\fR -or \fBTMPDIR\fR (see below). The SAT-solver should follow the convention -of the SAT Competition for its input and output format. +is used by the sat\-minimize option described above. The default +value is \f(CW"glucose -verb=0 %I >%O"\fR. The escape sequences +\f(CW%I\fR and \f(CW%O\fR respectively denote the names of the input +and output files. These temporary files are created in the directory +specified by \fBSPOT_TMPDIR\fR or \fBTMPDIR\fR (see below). The +SAT-solver should follow the convention of the SAT Competition for its +input and output format. .TP \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR diff --git a/src/misc/satsolver.cc b/src/misc/satsolver.cc index e9d351a9f..914fba7d1 100644 --- a/src/misc/satsolver.cc +++ b/src/misc/satsolver.cc @@ -40,7 +40,7 @@ namespace spot satsolver = getenv("SPOT_SATSOLVER"); if (!satsolver) { - satsolver = "glucose %I >%O"; + satsolver = "glucose -verb=0 %I >%O"; return; } prime(satsolver);