Fix side condition check in sygus core connective (#3600)

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index a8c4cb0d178166e963d5c80eb33ea0eaeb80a673..a924873d0976262550159c3c6168a1b1025d00f5 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -805,6 +805,10 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
           std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
+          for (const Node& sca : scasserts)
+          {
+            checkSc.assertFormula(sca.toExpr());
+          }
           Result rsc = checkSc.checkSat();
           Trace("sygus-ccore")
               << "----- check-sat returned " << rsc << std::endl;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9e3e04f0606bcb18c6619e274b03c476c34ab1de..03d38df5ef114c0ea455de6053c7de70d91bcf8a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1728,6 +1728,7 @@ set(regress_1_tests
   regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
   regress1/sygus/abd-simple-conj-4.smt2
+  regress1/sygus/abduction_1255.corecstrs.readable.smt2
   regress1/sygus/abduction_streq.readable.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array_search_5-Q-easy.sy

diff --git a/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
new file mode 100644 (file)
index 0000000..691cf6d
--- /dev/null
+++ b/test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
@@ -0,0 +1,76 @@
+; REQUIRES: proof
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+
+(set-info :smt-lib-version |2.6|)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2018-04-25
+Generator: Kudzu, converted to v2.6 by CVC4
+Application: Symbolic Execution of Javascript
+Target solver: Kaluza
+Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
+|)
+(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
+(set-info :category |"industrial"|)
+(set-info :status unknown)
+(declare-fun T_1 () Bool)
+(declare-fun T_10 () Bool)
+(declare-fun T_11 () Bool)
+(declare-fun T_12 () Bool)
+(declare-fun T_13 () Bool)
+(declare-fun T_14 () Bool)
+(declare-fun T_2 () Bool)
+(declare-fun T_3 () Bool)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun T_6 () Bool)
+(declare-fun T_7 () Bool)
+(declare-fun T_8 () Bool)
+(declare-fun T_9 () Bool)
+(declare-fun T_a () Bool)
+(declare-fun T_b () Bool)
+(declare-fun T_c () Bool)
+(declare-fun T_d () Bool)
+(declare-fun T_e () Bool)
+(declare-fun T_f () Bool)
+(declare-fun var_0xINPUT_245549 () String)
+(assert (= T_1 (not (= "6JX7G3VKFq" var_0xINPUT_245549))))
+(assert T_1)
+(assert (= T_2 (not (= "" var_0xINPUT_245549))))
+(assert T_2)
+(assert (= T_3 (not (= var_0xINPUT_245549 ""))))
+(assert T_3)
+(assert (= T_4 (not (= "" var_0xINPUT_245549))))
+(assert T_4)
+(assert (= T_5 (= var_0xINPUT_245549 "")))
+(assert (= T_6 (not T_5)))
+(assert T_6)
+(assert (= T_7 (not (= "" var_0xINPUT_245549))))
+(assert T_7)
+(assert (= T_8 (not (= "" var_0xINPUT_245549))))
+(assert T_8)
+(assert (= T_9 (not (= var_0xINPUT_245549 ""))))
+(assert T_9)
+(assert (= T_a (= var_0xINPUT_245549 "")))
+(assert (= T_b (not T_a)))
+(assert T_b)
+(assert (= T_c (not (= "" var_0xINPUT_245549))))
+(assert T_c)
+(assert (= T_d (not (= var_0xINPUT_245549 ""))))
+(assert T_d)
+(assert (= T_e (not (= "" var_0xINPUT_245549))))
+(assert T_e)
+(assert (= T_f (= var_0xINPUT_245549 "")))
+(assert (= T_10 (not T_f)))
+(assert T_10)
+(assert (= T_11 (not (= "" var_0xINPUT_245549))))
+(assert T_11)
+(assert (= T_12 (= var_0xINPUT_245549 "Example:")))
+(assert (= T_13 (not T_12)))
+(assert T_13)
+(assert (= T_14 (not (= var_0xINPUT_245549 "CQALcCP5TB"))))
+(get-abduct A (not T_14))