diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-23 10:23:00 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-23 10:23:00 -0600 |
| commit | 5aa585b74682a7e92a188548ce582eeb1212e42b (patch) | |
| tree | 5376b26f086474910ed70632b4a71dc6a32194d5 /src | |
| parent | e11af4be0f3d1dee41aefa91d856de9035cb3a29 (diff) | |
(proof-new) Miscellaneous changes from proof-new (#5445)
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 4 | ||||
| -rw-r--r-- | src/expr/type_node.cpp | 4 | ||||
| -rw-r--r-- | src/smt/preprocessor.cpp | 1 |
3 files changed, 5 insertions, 4 deletions
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); } |