diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-17 03:10:39 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-17 10:10:39 +0100 |
commit | 94334c412be47c1555e52d9e20a6ff5e18817249 (patch) | |
tree | 7975cb61152ce3536f20777c77020b09d1f2ccd7 /test/regress/regress0/fmf | |
parent | 80e02468be0b5821e74a097179299c9afa23d10a (diff) |
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.
Diffstat (limited to 'test/regress/regress0/fmf')
-rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
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) |