diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 11 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue5330.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue5330_2.smt2 | 9 |
4 files changed, 28 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1dc19deb1..a9e2c0051 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -337,8 +337,11 @@ bool TheoryStrings::collectModelInfoType( // is it an equivalence class with a seq.unit term? if (nfe.d_nf[0].getKind() == SEQ_UNIT) { - pure_eq_assign[eqc] = nfe.d_nf[0]; + Node c = Rewriter::rewrite(nm->mkNode( + SEQ_UNIT, d_valuation.getModelValue(nfe.d_nf[0][0]))); + pure_eq_assign[eqc] = c; Trace("strings-model") << "(unit: " << nfe.d_nf[0] << ") "; + m->getEqualityEngine()->addTerm(c); } // does it have a code and the length of these equivalence classes are // one? @@ -366,6 +369,12 @@ bool TheoryStrings::collectModelInfoType( else { processed[eqc] = eqc; + // Make sure that constants are asserted to the theory model that we + // are building. It is possible that new constants were introduced by + // the eager evaluation in the equality engine. These terms are missing + // in the term set and, as a result, are skipped when the equality + // engine is asserted to the theory model. + m->getEqualityEngine()->addTerm(eqc); } } Trace("strings-model") << "have length " << lts_values[i] << std::endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3bce17525..334901c7a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1845,6 +1845,8 @@ set(regress_1_tests regress1/strings/issue4735.smt2 regress1/strings/issue4735_2.smt2 regress1/strings/issue4759-comp-delta.smt2 + regress1/strings/issue5330.smt2 + regress1/strings/issue5330_2.smt2 regress1/strings/issue5374-proxy-i.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 diff --git a/test/regress/regress1/strings/issue5330.smt2 b/test/regress/regress1/strings/issue5330.smt2 new file mode 100644 index 000000000..aa0db8591 --- /dev/null +++ b/test/regress/regress1/strings/issue5330.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(declare-fun str1 () String) +(declare-fun str18 () String) +(assert (str.in_re (str.replace str18 str1 str18) (str.to_re "pANjvthXNyBbIgIlkC"))) +(check-sat) diff --git a/test/regress/regress1/strings/issue5330_2.smt2 b/test/regress/regress1/strings/issue5330_2.smt2 new file mode 100644 index 000000000..f67a95335 --- /dev/null +++ b/test/regress/regress1/strings/issue5330_2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(declare-fun seq11 () (Seq Int)) +(declare-fun i5 () Int) +(declare-fun v17 () Bool) +(declare-fun v24 () Bool) +(assert (xor v17 v24 true true (seq.prefixof (seq.rev (seq.rev seq11)) (seq.unit i5)))) +(check-sat) |