From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 24 Jul 2019 15:05:20 +0000 (-0500)
Subject:  Fix null node when using no-strings-lazy-pp (#3114)
X-Git-Tag: cvc5-1.0.0~4079
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=892718a5925075ad9024e2183060c4c25d2716e0;p=cvc5.git

 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 e3634f84f..d1eef656b 100644
--- 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 659071fc3..62672878e 100644
--- 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
index 000000000..672c4e5fc
--- /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)