diff options
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 7 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/no-lazy-pp-quant.smt2 | 9 |
3 files changed, 16 insertions, 1 deletions
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) |