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

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)