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/regress1/quantifiers | |
| 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/regress1/quantifiers')
10 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2 index d333358ed..b851d2e19 100644 --- a/test/regress/regress1/quantifiers/horn-simple.smt2 +++ b/test/regress/regress1/quantifiers/horn-simple.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer -q +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) 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 585ea0602..fdbac9996 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 -q +; COMMAND-LINE: --cegqi-bv ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/issue3664.smt2 b/test/regress/regress1/quantifiers/issue3664.smt2 index 0120f0e8a..28e999604 100644 --- a/test/regress/regress1/quantifiers/issue3664.smt2 +++ b/test/regress/regress1/quantifiers/issue3664.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun-rlv --sygus-inference -q +; COMMAND-LINE: --fmf-fun-rlv --sygus-inference ; EXPECT: sat (set-logic QF_NRA) (declare-fun a () Real) diff --git a/test/regress/regress1/quantifiers/issue4849-nqe.smt2 b/test/regress/regress1/quantifiers/issue4849-nqe.smt2 index dd7a22e39..4d0ce13fd 100644 --- a/test/regress/regress1/quantifiers/issue4849-nqe.smt2 +++ b/test/regress/regress1/quantifiers/issue4849-nqe.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-nested-qe -q +; COMMAND-LINE: --cegqi-nested-qe ; EXPECT: sat (set-logic LIA) (set-option :cegqi-nested-qe true) diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2 index 8846fe7fa..f414f4631 100644 --- a/test/regress/regress1/quantifiers/issue5470-aext.smt2 +++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -q +; COMMAND-LINE: ; EXPECT: sat (set-logic NIA) (set-option :strings-exp true) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 index d45d72253..9e8cd6586 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 index 2935de44d..af4d006c9 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 index 17028065c..2c42744ac 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 index 95608c150..f24aa6b1b 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 index 151499d78..dbb653351 100644 --- a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) |