From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Apr 2020 19:38:01 +0000 (-0500)
Subject: Remove a few spurious assertions (#4294)
X-Git-Tag: cvc5-1.0.0~3377
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7546557861686126b86a94fe797701afb1be4cd;p=cvc5.git

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 f81b0e160..e62de0840 100644
--- 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 66e80523a..1b3844578 100644
--- 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 799c23f5a..9608791f2 100644
--- 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
index 000000000..d9d9cc4a9
--- /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)