From ae82eb306143ade54a6f99b2aae0b62b8c77cd35 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 11 Jan 2021 08:48:01 -0600
Subject: 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.
---
 test/regress/CMakeLists.txt                     | 3 +++
 test/regress/regress0/nl/issue5737-div00.smt2   | 6 ++++++
 test/regress/regress0/nl/issue5740-2-mod00.smt2 | 8 ++++++++
 test/regress/regress0/nl/issue5740-mod00.smt2   | 7 +++++++
 4 files changed, 24 insertions(+)
 create mode 100644 test/regress/regress0/nl/issue5737-div00.smt2
 create mode 100644 test/regress/regress0/nl/issue5740-2-mod00.smt2
 create mode 100644 test/regress/regress0/nl/issue5740-mod00.smt2

(limited to 'test')

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)
-- 
cgit v1.2.3