Fix null node when using no-strings-lazy-pp (#3114)

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index e3634f84f7a60720fb80aac78b805a6189ddcdf8..d1eef656b6307ab7c61f50096f45e2add2ba05cc 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -607,6 +607,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       }
     }
   }
+  else
+  {
+    Trace("strings-preprocess-debug")
+        << "Return " << retNode << " unchanged" << std::endl;
+  }
   return retNode;
 }
 
@@ -615,7 +620,7 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st
   if( it!=visited.end() ){
     return it->second;
   }else{
-    Node retNode;
+    Node retNode = t;
     if( t.getNumChildren()==0 ){
       retNode = simplify( t, new_nodes );
     }else if( t.getKind()!=kind::FORALL ){

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 659071fc36cdda0bf1fe07b0a99baead7ad12692..62672878ed090370f4370a48ad8339a7a59d9127 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1567,6 +1567,7 @@ set(regress_1_tests
   regress1/strings/loop008.smt2
   regress1/strings/loop009.smt2
   regress1/strings/nf-ff-contains-abs.smt2
+  regress1/strings/no-lazy-pp-quant.smt2
   regress1/strings/non_termination_regular_expression4.smt2
   regress1/strings/norn-13.smt2
   regress1/strings/norn-360.smt2

diff --git a/test/regress/regress1/strings/no-lazy-pp-quant.smt2 b/test/regress/regress1/strings/no-lazy-pp-quant.smt2
new file mode 100644 (file)
index 0000000..672c4e5
--- /dev/null
+++ b/test/regress/regress1/strings/no-lazy-pp-quant.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun result () Int)
+(declare-fun s () String)
+(assert (! (not (= (str.to.int s) result)) :named a0))
+(check-sat)