Simplify and fix check models (#5685)

Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true.

However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base.

Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not.

This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions.

A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators.

Fixes #5645.

17 files changed, 29 insertions, 13 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 01903202c..d185049e0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -833,6 +833,7 @@ set(regress_0_tests
   regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
   regress0/quantifiers/issue4437-unc-quant.smt2
   regress0/quantifiers/issue4576.smt2
+  regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
diff --git a/test/regress/regress0/datatypes/issue1433.smt2 b/test/regress/regress0/datatypes/issue1433.smt2
index bac9b8af1..edbd6da69 100644
--- a/test/regress/regress0/datatypes/issue1433.smt2
+++ b/test/regress/regress0/datatypes/issue1433.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_UFDTLIA)
 (set-info :status sat)
 (declare-datatype MyList (par (T) ((nelem) (cons (hd T) (tl (MyList T))))))
diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2
index 21fa06270..749b0e218 100644
--- a/test/regress/regress0/decision/quant-ex1.smt2
+++ b/test/regress/regress0/decision/quant-ex1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --decision=justification
+; COMMAND-LINE: --decision=justification -q
 ; EXPECT: sat
 
 (set-logic AUFLIRA)
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
index 619779c78..32a75e846 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-option :incremental false)
 (set-info :status sat)
diff --git a/test/regress/regress0/fp/issue3536.smt2 b/test/regress/regress0/fp/issue3536.smt2
index 4293cbdee..68a17347e 100644
--- a/test/regress/regress0/fp/issue3536.smt2
+++ b/test/regress/regress0/fp/issue3536.smt2
@@ -1,4 +1,6 @@
 ; REQUIRES: symfpu
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_FP)
 (declare-const x (_ FloatingPoint 11 53))
 (assert (= true (fp.eq x ((_ to_fp 11 53) (_ bv13831004815617530266 64))) true))
diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2
index 9d6e0a36d..3e0858035 100644
--- a/test/regress/regress0/fp/issue3619.smt2
+++ b/test/regress/regress0/fp/issue3619.smt2
@@ -1,4 +1,6 @@
 ; REQUIRES: symfpu
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_FPLRA)
 (set-info :status sat)
 (declare-fun a () (_ FloatingPoint 11 53))
diff --git a/test/regress/regress0/parser/to_fp.smt2 b/test/regress/regress0/parser/to_fp.smt2
index 8652a5c33..277209ff8 100644
--- a/test/regress/regress0/parser/to_fp.smt2
+++ b/test/regress/regress0/parser/to_fp.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: --strict-parsing
+; COMMAND-LINE: --strict-parsing -q
 ; EXPECT: sat
 (set-logic QF_FP)
 (declare-fun |c::main::main::3::div@1!0&0#1| () (_ FloatingPoint 8 24))
diff --git a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
new file mode 100644
index 000000000..0d3f711bf
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((Enum1 0)) (((None) (cons (data Bool)))))
+(assert (forall ((var_1 Enum1)) (data var_1)))
+(check-sat)
diff --git a/test/regress/regress1/arith/arith-brab-test.smt2 b/test/regress/regress1/arith/arith-brab-test.smt2
index 7856ae0e6..4d87fdbae 100644
--- a/test/regress/regress1/arith/arith-brab-test.smt2
+++ b/test/regress/regress1/arith/arith-brab-test.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --arith-brab
-; COMMAND-LINE: --no-arith-brab
+; COMMAND-LINE: --arith-brab -q
+; COMMAND-LINE: --no-arith-brab -q
 ; EXPECT: sat
 (set-logic ALL)
 
diff --git a/test/regress/regress1/bug507.smt2 b/test/regress/regress1/bug507.smt2
index b93229dfe..0176d1043 100644
--- a/test/regress/regress1/bug507.smt2
+++ b/test/regress/regress1/bug507.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2
index 8ee89145b..0bc9fe2bb 100644
--- a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2
+++ b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-option :incremental false)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/am-bad-model.cvc b/test/regress/regress1/fmf/am-bad-model.cvc
index e30b5e04a..75d4e9f3d 100644
--- a/test/regress/regress1/fmf/am-bad-model.cvc
+++ b/test/regress/regress1/fmf/am-bad-model.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: sat
 OPTION "produce-models";
 OPTION "finite-model-find";
diff --git a/test/regress/regress1/fmf/refcount24.cvc.smt2 b/test/regress/regress1/fmf/refcount24.cvc.smt2
index e3b6957d0..2aaa28a3a 100644
--- a/test/regress/regress1/fmf/refcount24.cvc.smt2
+++ b/test/regress/regress1/fmf/refcount24.cvc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
index fdbac9996..585ea0602 100644
--- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
+++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv
+; COMMAND-LINE: --cegqi-bv -q
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/sets/choose3.smt2 b/test/regress/regress1/sets/choose3.smt2
index 744192496..2a844efeb 100644
--- a/test/regress/regress1/sets/choose3.smt2
+++ b/test/regress/regress1/sets/choose3.smt2
@@ -1,7 +1,9 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
 (set-option :produce-models true)
 (declare-fun A () (Set Int))
 (assert (= (choose A) 10))
 (assert (= A (as emptyset (Set Int))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
index 3636b5795..c674c4039 100644
--- a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
+++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
@@ -1,6 +1,6 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: --decision=internal
-; COMMAND-LINE: --decision=justification
+; COMMAND-LINE: --decision=internal -q
+; COMMAND-LINE: --decision=justification -q
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_BVFP)
@@ -12,4 +12,4 @@
 (assert (or (= k2 b) (= k2 a)))
 (assert
 (or (fp.isNaN ((_ to_fp 11 53) k2)) (fp.gt ((_ to_fp 11 53) k2) ((_ to_fp 11 53) (_ bv4626322717216342016 64))) ))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2
index 02f7754cf..5c4155b83 100644
--- a/test/regress/regress2/issue3687-check-models.smt2
+++ b/test/regress/regress2/issue3687-check-models.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --check-models
+; COMMAND-LINE: --check-models -q
 ; EXPECT: sat
 (set-logic QF_ABV)
 (declare-fun c () (_ BitVec 32))