diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-23 20:45:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-24 01:45:01 +0000 |
| commit | 8f50a5600e0664330128d2ac824092a685ef965e (patch) | |
| tree | ce3e08fbaa21cee663604e3da5981374d5b8da1a /test/regress/regress0/push-pop | |
| parent | 47c9c2f42696a1e04577c1a79ac78f4186657818 (diff) | |
Improve getValue for non-evaluated operators (#6436)
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
Diffstat (limited to 'test/regress/regress0/push-pop')
| -rw-r--r-- | test/regress/regress0/push-pop/real-as-int-incremental.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 b/test/regress/regress0/push-pop/real-as-int-incremental.smt2 index 155033d7d..81af8c4e7 100644 --- a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 +++ b/test/regress/regress0/push-pop/real-as-int-incremental.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --solve-real-as-int -q +; COMMAND-LINE: --incremental --solve-real-as-int ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat |