(proof-new) Miscellaneous changes from proof-new (#5445)

diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 02613345f8bdac2ceb332d6c19dc989a9a824902..858ca9f647f5dc75a483d78df22adbc047b541f4 100644 (file)
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -138,7 +138,9 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx)
   // should not rewrite term to two different things
   if (!getRewriteStepInternal(thash).isNull())
   {
-    Assert(getRewriteStepInternal(thash) == s);
+    Assert(getRewriteStepInternal(thash) == s)
+        << identify() << " rewriting " << t << " to both " << s << " and "
+        << getRewriteStepInternal(thash);
     return Node::null();
   }
   d_rewriteMap[thash] = s;

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 0818ca8c1ee35dea5d219d7bb21593eb850e013d..49fbe73eff4688016f5e13ad6280bba0baa426e9 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -589,13 +589,11 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
     case kind::SEQUENCE_TYPE:
     case kind::SET_TYPE:
     case kind::BAG_TYPE:
+    case kind::SEXPR_TYPE:
     {
       // we don't support subtyping except for built in types Int and Real.
       return TypeNode();  // return null type
     }
-    case kind::SEXPR_TYPE:
-      Unimplemented()
-          << "haven't implemented leastCommonType for symbolic expressions yet";
     default:
       Unimplemented() << "don't have a commonType for types `" << t0
                       << "' and `" << t1 << "'";

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 98a2a7a36237e634254076f1a87a7c4f4e8b70dc..5a1ce63a4af41b9241f2d720bfe7d3b598b40136 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -158,6 +158,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
 {
   Assert(pppg != nullptr);
   d_pnm = pppg->getManager();
+  d_propagator.setProof(d_pnm, d_context, pppg);
   d_rtf.setProofNodeManager(d_pnm);
 }