diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-11 08:48:01 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-11 08:48:01 -0600 |
| commit | ae82eb306143ade54a6f99b2aae0b62b8c77cd35 (patch) | |
| tree | 1ad4dadb2ada741fbd6d43e7755a81204eadea23 /test/regress | |
| parent | fcac065b47ea73aecb90f019c07dc6fa09cd914f (diff) | |
Remove extended rewrite for arithmetic (#5760)
This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.
Fixes #5737, fixes #5740.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/nl/issue5737-div00.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress0/nl/issue5740-2-mod00.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress0/nl/issue5740-mod00.smt2 | 7 |
4 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 7ceb3b4b2..dd6956b09 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -686,6 +686,9 @@ set(regress_0_tests regress0/nl/issue5534-no-assertions.smt2 regress0/nl/issue5726-downpolys.smt2 regress0/nl/issue5726-sqfactor.smt2 + regress0/nl/issue5737-div00.smt2 + regress0/nl/issue5740-mod00.smt2 + regress0/nl/issue5740-2-mod00.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 diff --git a/test/regress/regress0/nl/issue5737-div00.smt2 b/test/regress/regress0/nl/issue5737-div00.smt2 new file mode 100644 index 000000000..59de5a3fb --- /dev/null +++ b/test/regress/regress0/nl/issue5737-div00.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --ext-rew-prep -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (> (div 0 0) 0)) +(check-sat) diff --git a/test/regress/regress0/nl/issue5740-2-mod00.smt2 b/test/regress/regress0/nl/issue5740-2-mod00.smt2 new file mode 100644 index 000000000..01930da6d --- /dev/null +++ b/test/regress/regress0/nl/issue5740-2-mod00.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ext-rewrite-quant --sygus-inst --no-check-models +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun c (Int) Bool) +(define-fun d ((e Int)) Bool (forall ((a Int) (b Int)) (! true :pattern ((c a) (c b))))) +(assert (exists ((e Int)) (distinct (d e) (= (ite (= e 0) (mod 0 e) 0) 0)))) +(check-sat) diff --git a/test/regress/regress0/nl/issue5740-mod00.smt2 b/test/regress/regress0/nl/issue5740-mod00.smt2 new file mode 100644 index 000000000..e1287dacb --- /dev/null +++ b/test/regress/regress0/nl/issue5740-mod00.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --ext-rewrite-quant -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(define-fun f ((a Int) (b Int)) Int (ite (= b 0) 0 a)) +(assert (exists ((c Int)) (distinct (f c (mod 0 0)) 0))) +(check-sat) |