diff options
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 1 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sets/issue4124-need-check.smt2 | 13 |
4 files changed, 17 insertions, 2 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5558b95d4..0d1206dec 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -981,7 +981,6 @@ void TheorySetsPrivate::computeCareGraph() // populate indices for (TNode f1 : it.second) { - Assert(d_equalityEngine->hasTerm(f1)); Trace("sets-cg-debug") << "...build for " << f1 << std::endl; Assert(d_equalityEngine->hasTerm(f1)); // break into index based on operator, and type of first argument (since diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0fd8347c8..9ba97fa77 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -504,7 +504,9 @@ void TheoryEngine::check(Theory::Effort effort) { propagate(effort); // We do combination if all has been processed and we are in fullcheck - if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) { + if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() + && !d_factsAsserted && !needCheck() && !d_inConflict) + { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl; { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e158f629a..82ef8702a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1953,6 +1953,7 @@ set(regress_1_tests regress1/sets/is_singleton1.smt2 regress1/sets/issue2568.smt2 regress1/sets/issue2904.smt2 + regress1/sets/issue4124-need-check.smt2 regress1/sets/issue4391-card-lasso.smt2 regress1/sets/issue5271.smt2 regress1/sets/issue5309.smt2 diff --git a/test/regress/regress1/sets/issue4124-need-check.smt2 b/test/regress/regress1/sets/issue4124-need-check.smt2 new file mode 100644 index 000000000..3ad43ea98 --- /dev/null +++ b/test/regress/regress1/sets/issue4124-need-check.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --sets-infer-as-lemmas --simplification=none +; EXPECT: sat +(set-logic ALL) +(declare-fun b () (Set (Tuple String Int))) +(declare-fun c () (Set (Tuple Int String))) +(declare-fun d () (Set (Tuple String String))) +(declare-fun f () (Set Int)) +(declare-fun e () Int) +(assert (= b (insert (mkTuple "" 1) (mkTuple "" 2) (singleton (mkTuple "" 4))))) +(assert (= c (insert (mkTuple 1 "1") (mkTuple 2 "2") (singleton (mkTuple 7 ""))))) +(assert (= d (join b c))) +(assert (= e (card f))) +(check-sat) |