Fix explanation for strings unit oob inference (#8908)

Fixes #8906.

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 998926802d17593d680fd54d12b8581ec705348c..0c01e8316bbfc4de3d090e668cf07164c8027bf4 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -151,8 +151,14 @@ void BaseSolver::checkInit()
                   Node scr = utils::mkCodeRange(s, d_cardSize);
                   Node tcr = utils::mkCodeRange(t, d_cardSize);
                   Node conc = nm->mkNode(OR, scr.notNode(), tcr.notNode());
+                  // We do not explain exp for two reasons. First, we are
+                  // caching this inference based on the user context and thus
+                  // it should not depend on the current explanation. Second,
+                  // s or t may be concrete integers corresponding to code
+                  // points of string constants, and thus are not guaranteed to
+                  // be terms in the equality engine.
                   d_im.sendInference(
-                      exp, conc, InferenceId::STRINGS_UNIT_INJ_OOB);
+                      exp, exp, conc, InferenceId::STRINGS_UNIT_INJ_OOB);
                 }
               }
               else

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index d2f6b242fa9d08a70cdabddcab47ca14f0133c18..131089219affde965e580eee49ba3aaa36a820c1 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1277,6 +1277,7 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity,
 
 void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
 {
+  Trace("eq-exp") << "explainLit: " << lit << std::endl;
   Assert(lit.getKind() != kind::AND);
   bool polarity = lit.getKind() != kind::NOT;
   TNode atom = polarity ? lit : lit[0];

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index eeeae8692d99ccf8b7c1a83a99d03f6df171ba41..1ced25e3cc895b23766bdcbd5268b272abaacd95 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2627,6 +2627,7 @@ set(regress_1_tests
   regress1/strings/issue8347-has-skolem.smt2
   regress1/strings/issue8434-nterm-str-rw.smt2
   regress1/strings/issue8890-inj-oob.smt2
+  regress1/strings/issue8906-oob-exp.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/cli/regress1/strings/issue8906-oob-exp.smt2 b/test/regress/cli/regress1/strings/issue8906-oob-exp.smt2
new file mode 100644 (file)
index 0000000..d2a61fa
--- /dev/null
+++ b/test/regress/cli/regress1/strings/issue8906-oob-exp.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unknown
+(set-logic ALL)
+(declare-const x1 Bool)
+(declare-const x Int)
+(assert (forall ((e String)) (or (exists ((e String)) (or (ite (str.prefixof "-" (str.at e 0)) false (= 1 (str.to_int (str.at e (+ x (str.len e)))))) x1)))))
+(check-sat)