From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jan 2020 22:02:38 +0000 (-0600)
Subject: Make eq chain an aggressive rewrite in extended rewriter (#3679)
X-Git-Tag: cvc5-1.0.0~3705
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c4788b6356b46df5cede71bcf02c86f0aebe86c;p=cvc5.git

Make eq chain an aggressive rewrite in extended rewriter (#3679)
---

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 0fbd971fd..05e789ce2 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -1137,6 +1137,13 @@ Node ExtendedRewriter::extendedRewriteEqChain(
 {
   Assert(ret.getKind() == eqk);
 
+  // this rewrite is aggressive; it in fact has the precondition that other
+  // aggressive rewrites (including BCP) have been applied.
+  if (!d_aggr)
+  {
+    return Node::null();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
 
   TypeNode tn = ret[0].getType();
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 799219eec..179c5fe4c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1284,6 +1284,7 @@ set(regress_1_tests
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
   regress1/nl/issue3441.smt2
+  regress1/nl/issue3656.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2
diff --git a/test/regress/regress1/nl/issue3656.smt2 b/test/regress/regress1/nl/issue3656.smt2
new file mode 100644
index 000000000..6de6e26b9
--- /dev/null
+++ b/test/regress/regress1/nl/issue3656.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --ext-rew-prep
+; EXPECT: sat
+(set-logic QF_NRA)   
+(set-info :status sat)  
+(declare-fun b () Real)
+(declare-fun c () Real)
+(assert (distinct (and (>= c (* c c c c)) (< c (* c c c c))) (= (* b c) 0.0)))
+(check-sat)