Fix strings preprocessing for justification heuristic

2 files changed, 12 insertions, 4 deletions

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 51ad7b6ca..c9c3d6345 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -83,9 +83,9 @@ assertions\n\
 + Output the assertions after preprocessing and before clausification.\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
   where PASS is one of the preprocessing passes: definition-expansion\n\
-  boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
-  static-learning ite-removal repeat-simplify rewrite-apply-to-const\n\
-  theory-preprocessing.\n\
+  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+  simplify static-learning ite-removal repeat-simplify\n\
+  rewrite-apply-to-const theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
   \"assertions:pre-everything\") or after all preprocessing completes\n\
@@ -181,6 +181,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
       } else if(!strcmp(p, "boolean-terms")) {
       } else if(!strcmp(p, "constrain-subtypes")) {
       } else if(!strcmp(p, "substitution")) {
+      } else if(!strcmp(p, "strings-pp")) {
       } else if(!strcmp(p, "skolem-quant")) {
       } else if(!strcmp(p, "simplify")) {
       } else if(!strcmp(p, "static-learning")) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dcca1624d..ec91e566e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3124,11 +3124,18 @@ void SmtEnginePrivate::processAssertions() {
   // Assertions ARE guaranteed to be rewritten by this point
 
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+    dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
     CVC4::theory::strings::StringsPreprocess sp;
-    sp.simplify( d_assertionsToPreprocess );
+    std::vector<Node> newNodes;
+    newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
+    sp.simplify( d_assertionsToPreprocess, newNodes );
+    if(newNodes.size() > 1) {
+      d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
+    }
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
       d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
     }
+    dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
   }
   if( d_smt.d_logic.isQuantified() ){
     dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);