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/regress0/nl/issue5740-2-mod00.smt2 | |
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/regress0/nl/issue5740-2-mod00.smt2')
-rw-r--r-- | test/regress/regress0/nl/issue5740-2-mod00.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
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) |