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 07:43:30 +02:00
parent 3f3d058567
commit 9958cab5cc
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_pb.cpp
View file

@ -1882,9 +1882,8 @@ namespace smt {
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)) { if (cjs && !is_proof_justification(*cjs)) {
TRACE("pb", tout << "skipping justification for clause over: " << conseq << " " TRACE("pb", tout << "not processing justification over: " << conseq << " " << typeid(*cjs).name() << "\n";);
<< typeid(*cjs).name() << "\n";); return false;
break;
} }
unsigned num_lits = cls.get_num_literals(); unsigned num_lits = cls.get_num_literals();
if (cls.get_literal(0) == conseq) { if (cls.get_literal(0) == conseq) {