diff options
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 21 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2 | 7 |
3 files changed, 21 insertions, 8 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 7737a90f7..0db536d1b 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -284,16 +284,21 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) } InferenceId inf = polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG; - d_im.sendInference(iexp, noExplain, conc, inf); - addedLemma = true; - processed.push_back(assertion); - if (e == 0) + // in very rare cases, we may find out that the unfolding lemma + // for a membership is equivalent to true, in spite of the RE + // not being rewritten to true. + if (d_im.sendInference(iexp, noExplain, conc, inf)) { - // Remember that we have unfolded a membership for x - // notice that we only do this here, after we have definitely - // added a lemma. - repUnfold.insert(rep); + addedLemma = true; + if (e == 0) + { + // Remember that we have unfolded a membership for x + // notice that we only do this here, after we have definitely + // added a lemma. + repUnfold.insert(rep); + } } + processed.push_back(assertion); } else { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 64c584f7a..81c2bdba3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1111,6 +1111,7 @@ set(regress_0_tests regress0/strings/issue5771-eager-pp.smt2 regress0/strings/issue5816-re-kind.smt2 regress0/strings/issue5915-repl-ctn-rewrite.smt2 + regress0/strings/issue6203-3-unfold-trivial-true.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2 b/test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2 new file mode 100644 index 000000000..1ef762df3 --- /dev/null +++ b/test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun s () String) +(assert (str.in_re s (re.* (re.union (str.to_re "A") (str.to_re s))))) +(assert (not (str.in_re s (re.* (re.opt (re.comp (str.to_re "A"))))))) +(check-sat) |