Unexpected verbose output when sat.cut=true #7639

cions · 2025-05-03T01:25:54Z

When enabling the sat.cut option, the solver prints a line like "#don't cares 178" even if verbose=0. I believe the output should be quiet at verbosity level 0.

The line responsible appears to be

z3/src/sat/sat_aig_cuts.cpp

Line 791 in dd211ba

IF_VERBOSE(0, verbose_stream() << "#don't cares " << dont_cares << "\n");

Additionally, when grepping the codebase for IF_VERBOSE, it seems there are several other places where output is emitted even if verbose=0. Furthermore, the verbosity level conventions appear to be inconsistent across the codebase.

Would it make sense to adopt a more consistent verbosity standard, such as: 0=quiet, 1=warning, 2=info, 3=debug

Code to reproduce

(set-info :status unknown)
(set-option :sat.cut true)
(set-option :verbose 0)
(declare-fun x () (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert
  (let ((smul (bvmul ((_ sign_extend 16) x) ((_ sign_extend 16) y)))
        (umul (bvmul ((_ zero_extend 16) x) ((_ zero_extend 16) y)))
        (sub1 (concat (ite (bvslt x (_ bv0 16)) y (_ bv0 16)) (_ bv0 16)))
        (sub2 (concat (ite (bvslt y (_ bv0 16)) x (_ bv0 16)) (_ bv0 16))))
    (not (= smul (bvsub (bvsub umul sub1) sub2)))))
(check-sat)

NikolajBjorner closed this as completed in 0e4c033 May 3, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Unexpected verbose output when sat.cut=true #7639

Unexpected verbose output when sat.cut=true #7639

Unexpected verbose output when sat.cut=true #7639

Unexpected verbose output when sat.cut=true #7639

Comments

Code to reproduce