diff options
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 14 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress3/strings/unsat-circ-reduce.smt2 | 13 |
3 files changed, 25 insertions, 3 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 55985406e..dd4144313 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -235,6 +235,8 @@ void ExtfSolver::checkExtfEval(int effort) NodeManager* nm = NodeManager::currentNM(); bool has_nreduce = false; std::vector<Node> terms = d_extt.getActive(); + // the set of terms we have done extf inferences for + std::unordered_set<Node, NodeHashFunction> inferProcessed; for (const Node& n : terms) { // Setup information about n, including if it is equal to a constant. @@ -415,16 +417,22 @@ void ExtfSolver::checkExtfEval(int effort) effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N; d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer); } - to_reduce = nrc; + // We must use the original n here to avoid circular justifications for + // why extended functions are reduced below. In particular, to_reduce + // should never be a duplicate of another term considered in the block + // of code for checkExtfInference below. + to_reduce = n; } } else { to_reduce = n; } - // if not reduced - if (!to_reduce.isNull()) + // if not reduced and not processed + if (!to_reduce.isNull() + && inferProcessed.find(to_reduce) == inferProcessed.end()) { + inferProcessed.insert(to_reduce); Assert(effort < 3); if (effort == 1) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 656bb5880..38b741ced 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2114,6 +2114,7 @@ set(regress_3_tests regress3/sixfuncs.sy regress3/strings-any-term.sy regress3/strings/extf_d_perf.smt2 + regress3/strings/unsat-circ-reduce.smt2 ) #-----------------------------------------------------------------------------# diff --git a/test/regress/regress3/strings/unsat-circ-reduce.smt2 b/test/regress/regress3/strings/unsat-circ-reduce.smt2 new file mode 100644 index 000000000..b584c0fb1 --- /dev/null +++ b/test/regress/regress3/strings/unsat-circ-reduce.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strings-exp --no-re-elim +; EXPECT: unsat +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () String) +(assert (not (= +(let ((_let_0 (re.* re.allchar ))) +(str.in_re x (re.++ re.allchar _let_0 (str.to_re "AC") _let_0 (str.to_re "CA") _let_0))) +(let ((_let_0 (+ 0 1))) (let ((_let_1 (str.indexof x "AC" _let_0))) (and (not (= _let_1 (- 1))) (not (= (str.indexof x "CA" (+ _let_1 (str.len "AC"))) (- 1)))))) +))) +(assert (<= (str.len x) 8)) +; adding --strings-fmf to command line above incorrectly said "sat" for this at ad0b69e6 +(check-sat) |