From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 25 Jan 2022 04:33:13 +0000 (-0800)
Subject: [Strings] Avoid trivial explanation (#7982)
X-Git-Tag: cvc5-1.0.0~509
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18c55e25574ef9dab5af7cdb86ad497d97b40911;p=cvc5.git

[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 84fd3af71..96cbf8848 100644
--- 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 1850fdda4..d89d7f344 100644
--- 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
index 000000000..22af48935
--- /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)