Remove a few spurious assertions (#4294)

Fixes #4290 and fixes #4292.

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index f81b0e1604af8c6d5037375a58388840e9715946..e62de0840c4ee662ba7c03fc8b6ed7b7f050da7b 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1151,8 +1151,8 @@ bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& no
 
 Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
                                          std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) {
+  n = Rewriter::rewrite(n);
   computeProgVars( n );
-  Assert(n == Rewriter::rewrite(n));
   bool is_basic = canApplyBasicSubstitution( n, non_basic );
   if( Trace.isOn("cegqi-si-apply-subs-debug") ){
     Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 66e80523a65cd431f951994f856ad8bbc85c61aa..1b38445784cbbb51a632e70d4f108da3938b523c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -68,7 +68,7 @@ bool SynthConjectureProcessFun::checkMatch(
   Node cn_subs =
       cn.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
   cn_subs = Rewriter::rewrite(cn_subs);
-  Assert(Rewriter::rewrite(n) == n);
+  n = Rewriter::rewrite(n);
   return cn_subs == n;
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 799c23f5ac2d9728d89fa22184258c244385429c..9608791f2486f4f8e57ff6217138b761c3ce8a48 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1519,6 +1519,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3765-quant-dd.smt2
   regress1/quantifiers/issue4021-ind-opts.smt2
   regress1/quantifiers/issue4062-cegqi-aux.smt2
+  regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2

diff --git a/test/regress/regress1/quantifiers/issue4290-cegqi-r.smt2 b/test/regress/regress1/quantifiers/issue4290-cegqi-r.smt2
new file mode 100644 (file)
index 0000000..d9d9cc4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4290-cegqi-r.smt2
@@ -0,0 +1,7 @@
+(set-logic AUFLIA)
+(set-info :status unsat)
+(declare-fun _substvar_29_ () (Array Bool Int))
+(declare-fun _substvar_55_ () (Array Bool Int))
+(declare-const arr-8129271443090794560_6381925390096970410-0 (Array Bool Int))
+(assert (not (exists ((q1 Int) (q2 Bool) (q3 (Array Bool Int))) (xor (distinct q1 51) (xor true true true true true true true true (= _substvar_29_ arr-8129271443090794560_6381925390096970410-0 (store _substvar_55_ true 70)) true true) true))))
+(check-sat)