mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

interpolation fix for commutativity

Browse source
This commit is contained in:
Ken McMillan 2014-02-19 13:56:55 -08:00
parent 76fb66314b
commit c9cf658e7c
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/interp/iz3proof_itp.cpp
View file

@ -2146,8 +2146,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
/** Make a Reflexivity node. This rule produces |- x = x */ /** Make a Reflexivity node. This rule produces |- x = x */
virtual node make_reflexivity(ast con){ virtual node make_reflexivity(ast con){
throw proof_error(); if(get_term_type(con) == LitA)
} return mk_false();
if(get_term_type(con) == LitB)
return mk_true();
ast itp = make(And,make(contra,no_proof,mk_false()),
make(contra,mk_true(),mk_not(con)));
return itp;
}
/** Make a Symmetry node. This takes a derivation of |- x = y and /** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x. Ditto for ~(x=y) */ produces | y = x. Ditto for ~(x=y) */