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/regress1/arith | |
| 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/regress1/arith')
| -rw-r--r-- | test/regress/regress1/arith/arith-brab-test.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
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) |