mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-08 16:25:48 +00:00
Code Activity

handle proof-wrapper justifications

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-16 11:25:50 +02:00
parent e38729a1c6
commit 1ca44ed316
2 changed files with 19 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_pb.h
View file

@ -157,6 +157,7 @@ namespace smt {
void process_antecedent(literal l, numeral coeff);
void process_ineq(ineq& c, literal conseq, numeral coeff);
void remove_from_lemma(ineq& c, unsigned idx);
bool is_proof_justification(justification const& j) const;
void hoist_maximal_values();