[Strings] Avoid trivial explanation (#7982)

The `STRINGS_N_UNIFY` inference could produce trivial explanations. For
example, if both `x` and `y` were of kind `seq.unit`, then the
explanation was `(= 1 1)`. This lead to issues when checking proofs.

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 84fd3af717760a18c8768176d30eaa4d47c09ff3..96cbf8848374ac3b47a7aaea938321f09cb3cd77 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1313,8 +1313,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       Trace("strings-solve-debug")
           << "Simple Case 2 : string lengths are equal" << std::endl;
       Node eq = x.eqNode(y);
-      Node leneq = xLenTerm.eqNode(yLenTerm);
-      lenExp.push_back(leneq);
+      d_im.addToExplanation(xLenTerm, yLenTerm, lenExp);
       // set the explanation for length
       Node lant = utils::mkAnd(lenExp);
       ant.push_back(lant);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1850fdda46ce7e02fdf3ca432843fcf5593b1385..d89d7f3445c85240deb87879a9ab1c09e09e29a0 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2727,6 +2727,7 @@ set(regress_2_tests
   regress2/quantifiers/nunchaku2309663.nun.min.smt2
   regress2/quantifiers/small-bug1-fixpoint-3.smt2
   regress2/quantifiers/syn874-1.smt2
+  regress2/seq/err-model-soundness.smt2
   regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
   regress2/strings/bidir_star.smt2
   regress2/strings/cmi-split-cm-fail.smt2

diff --git a/test/regress/regress2/seq/err-model-soundness.smt2 b/test/regress/regress2/seq/err-model-soundness.smt2
new file mode 100644 (file)
index 0000000..22af489
--- /dev/null
+++ b/test/regress/regress2/seq/err-model-soundness.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --strings-exp
+(set-logic ALL)
+(declare-sort E 0)
+(declare-fun x () (Seq E))
+(declare-fun y () (Seq E))
+(declare-fun z () (Seq E))
+(declare-fun e () E)
+(declare-fun d () E)
+
+(declare-fun x07 () (Seq E))
+(declare-fun x09 () (Seq E))
+(declare-fun x10 () (Seq E))
+(declare-fun x11 () (Seq E))
+
+
+(assert (= y (seq.update x09 0 (seq.unit d))))
+(assert (= y (seq.update y 0 (seq.unit (seq.nth x 0)))))
+(assert (= y (seq.update y 0 (seq.unit (seq.nth y 1)))))
+(assert (= z (seq.update z 0 (seq.unit (seq.nth z 1)))))
+
+(assert (= x07 (seq.update z 1 (seq.unit (seq.nth z (- 1))))))
+(assert (= x09 (seq.update x 0 (seq.unit e))))
+(assert (= x09 (seq.update x09 1 (seq.unit (seq.nth z 0)))))
+(assert (= x09 (seq.update x09 1 (seq.unit (seq.nth y (- 1))))))
+(assert (= x09 (seq.update z 0 (seq.unit e))))
+(assert (= x10 (seq.update z 0 (seq.unit (seq.nth z (- 1))))))
+(assert (= x11 (seq.update z 0 (seq.unit (seq.nth x07 (- 1))))))
+
+(assert (distinct x10 x11))
+(set-info :status unsat)
+(check-sat)