merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.cpp

@@ -1557,6 +1557,16 @@ std::ostream& ast_manager::display(std::ostream& out, parameter const& p) {
 }
 
 
+std::ostream& ast_manager::display(std::ostream& out, parameter const& p) {
+    switch (p.get_kind()) {
+    case parameter::PARAM_AST:
+        return out << mk_pp(p.get_ast(), *this);
+    default:
+        return p.display(out);
+    }
+    return out;
+}
+
 void ast_manager::copy_families_plugins(ast_manager const & from) {
     TRACE("copy_families_plugins",
           tout << "target:\n";

src/ast/ast.h

@@ -2586,6 +2586,16 @@ public:
     void operator()(AST * n) { m_manager.inc_ref(n); }
 };
 
+struct parameter_pp {
+    parameter const& p;
+    ast_manager& m;
+    parameter_pp(parameter const& p, ast_manager& m): p(p), m(m) {}
+};
+
+inline std::ostream& operator<<(std::ostream& out, parameter_pp const& pp) {
+    return pp.m.display(out, pp.p);
+}
+
 
 #endif /* AST_H_ */
 

src/ast/rewriter/seq_rewriter.cpp

@@ -859,10 +859,6 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         result = m_util.str.mk_concat(c, a);
         return BR_REWRITE1;
     }
-    if (m_util.str.is_string(a, s1) && s1.length() == 0) {
-        result = a;
-        return BR_DONE;
-    }
     return BR_FAILED;
 }