mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

fix #5808

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-02-07 20:10:32 +02:00
parent 9958cab5cc
commit 0059e88036
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_pb.cpp
View file

@ -1881,11 +1881,13 @@ namespace smt {
inc_coeff(conseq, offset); inc_coeff(conseq, offset);
clause& cls = *js.get_clause(); clause& cls = *js.get_clause();
justification* cjs = cls.get_justification(); justification* cjs = cls.get_justification();
if (cjs && !is_proof_justification(*cjs)) {
TRACE("pb", tout << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";);
return false;
}
unsigned num_lits = cls.get_num_literals(); unsigned num_lits = cls.get_num_literals();
if (cjs && typeid(smt::unit_resolution_justification) == typeid(*cjs))
;
else if (cjs && !is_proof_justification(*cjs)) {
TRACE("pb", tout << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";);
break;
}
if (cls.get_literal(0) == conseq) { if (cls.get_literal(0) == conseq) {
process_antecedent(cls.get_literal(1), offset); process_antecedent(cls.get_literal(1), offset);
} }