Strings: Make EXTF_d inference more conservative (#2740)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9da6fd2774ac5381362df38a861502a80850853a..5179ddab3dd834271e8c2cfd8fa476886c6b2ef8 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1662,9 +1662,9 @@ void TheoryStrings::checkExtfEval( int effort ) {
                               << ", const = " << einfo.d_const << std::endl;
         for (const Node& nrcc : nrc)
         {
-          sendInference(einfo.d_exp,
-                        einfo.d_const == d_false ? nrcc.negate() : nrcc,
-                        effort == 0 ? "EXTF_d" : "EXTF_d-N");
+          sendInternalInference(einfo.d_exp,
+                                einfo.d_const == d_false ? nrcc.negate() : nrcc,
+                                effort == 0 ? "EXTF_d" : "EXTF_d-N");
         }
       }else{
         to_reduce = nrc;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e0e57acf9bfd3673b2c8b9e2d4f5ae364a95526d..f22796929256b1b46550ca161110612a76e546da 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1729,6 +1729,7 @@ set(regress_2_tests
   regress2/strings/cmu-disagree-0707-dd.smt2
   regress2/strings/cmu-prereg-fmf.smt2
   regress2/strings/cmu-repl-len-nterm.smt2
+  regress2/strings/extf_d_perf.smt2
   regress2/strings/issue918.smt2
   regress2/strings/non_termination_regular_expression6.smt2
   regress2/strings/norn-dis-0707-3.smt2

diff --git a/test/regress/regress2/strings/extf_d_perf.smt2 b/test/regress/regress2/strings/extf_d_perf.smt2
new file mode 100644 (file)
index 0000000..7ad094d
--- /dev/null
+++ b/test/regress/regress2/strings/extf_d_perf.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --strings-exp --strings-fmf
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun _substvar_140_ () String)
+(declare-fun _substvar_195_ () Int)
+(declare-fun _substvar_201_ () Int)
+(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3)))))
+  (and
+    (str.contains _substvar_140_ "://")
+    (str.contains _let_3 "@")
+    (str.contains _let_5 ",")
+    (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0))
+    (not (= (str.len _let_4) 0))
+    (not (str.contains _let_0 ".sock"))
+    (not (str.contains _let_4 "@"))
+    (not (= (str.len _let_5) 0))
+    (= "mongodb://" (str.substr _substvar_140_ 0 10))))))))
+(check-sat)
+