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 0fbd971fd7b15702b5eb8e556d6d4e448ce38ec5..05e789ce292f1cfa718128b900a13c1776c8a3c8 100644 (file)
--- 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 799219eec9dccf71f343860a3a3e2fb537f31502..179c5fe4c43164b5d40caae7f2c938b96405c8f5 100644 (file)
--- 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 (file)
index 0000000..6de6e26
--- /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)