diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 | 76 |
3 files changed, 81 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index a8c4cb0d1..a924873d0 100644 --- 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 9e3e04f06..03d38df5e 100644 --- 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 index 000000000..691cf6d9a --- /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)) |