fix #4219

NikolajBjorner · NikolajBjorner · commit 2d08baf3d577 · 2020-05-06T12:20:40.000-07:00
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
@@ -2044,7 +2044,7 @@ namespace smt {
     }
 
     bool theory_pb::is_proof_justification(justification const& j) const {
-        return typeid(smt::justification_proof_wrapper) == typeid(j);
+        return typeid(smt::justification_proof_wrapper) == typeid(j) || get_manager().proofs_enabled();           
     }
 
     justification* theory_pb::justify(literal l1, literal l2) {

Original file line number	Diff line number	Diff line change
`@@ -2044,7 +2044,7 @@ namespace smt {`
`2044`	`2044`	`}`
`2045`	`2045`
`2046`	`2046`	`bool theory_pb::is_proof_justification(justification const& j) const {`
`2047`		`- return typeid(smt::justification_proof_wrapper) == typeid(j);`
	`2047`	`+ return typeid(smt::justification_proof_wrapper) == typeid(j) \|\| get_manager().proofs_enabled();`
`2048`	`2048`	`}`
`2049`	`2049`
`2050`	`2050`	`justification* theory_pb::justify(literal l1, literal l2) {`