From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Nov 2020 16:23:00 +0000 (-0600)
Subject: (proof-new) Miscellaneous changes from proof-new (#5445)
X-Git-Tag: cvc5-1.0.0~2559
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5aa585b74682a7e92a188548ce582eeb1212e42b;p=cvc5.git

(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 02613345f..858ca9f64 100644
--- 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 0818ca8c1..49fbe73ef 100644
--- 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 98a2a7a36..5a1ce63a4 100644
--- 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);
 }