diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 11:44:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 11:44:35 -0600 |
| commit | 3654512dd8b341c5725e550d438b23508493b991 (patch) | |
| tree | 367684e5521e35a452ef669a4e58bb1b5005509c /test/regress | |
| parent | b0130a1e032c201fab3c4b19f25871428b761967 (diff) | |
Fix issues related to eliminating extended arithmetic operators (#5475)
This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.
Fixes #5469, fixes #5470, fixes #5471.
This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.
This also improves our assertions and trace messages.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5469-aext.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5470-aext.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5471-aext.smt2 | 10 |
4 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b12876a5c..9935adf59 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1609,6 +1609,9 @@ set(regress_1_tests regress1/quantifiers/issue4620-erq-witness-unsound.smt2 regress1/quantifiers/issue4685-wrewrite.smt2 regress1/quantifiers/issue5019-cegqi-i.smt2 + regress1/quantifiers/issue5469-aext.smt2 + regress1/quantifiers/issue5470-aext.smt2 + regress1/quantifiers/issue5471-aext.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue5469-aext.smt2 b/test/regress/regress1/quantifiers/issue5469-aext.smt2 new file mode 100644 index 000000000..d66afb91a --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5469-aext.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --sygus-inst --strings-exp --no-check-models +; EXPECT: sat +(set-logic NIA) +(set-option :sygus-inst true) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun d () Int) +(assert (forall ((g Int)) (or (> 1 g) (> g (div 1 d))))) +(assert (not (= d 0))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2 new file mode 100644 index 000000000..500ef6d4c --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2 @@ -0,0 +1,6 @@ +(set-logic NIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun b () Int) +(assert (exists ((c Int)) (< 0 c (div 0 b)))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5471-aext.smt2 b/test/regress/regress1/quantifiers/issue5471-aext.smt2 new file mode 100644 index 000000000..c420359fc --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5471-aext.smt2 @@ -0,0 +1,10 @@ +(set-logic NRA) +(set-option :sygus-inst true) +(set-option :strings-exp true) +(set-info :status unsat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(assert (forall ((d Real)) (= (> d 0) (<= (+ d (/ a c)) 0)))) +(assert (<= (* b b) 0)) +(check-sat) |