mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fixing labels in duality

Browse source
This commit is contained in:
Ken McMillan 2013-05-22 15:42:25 -07:00
parent 9d611997b3
commit 058c8d2083
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/duality/duality_rpfp.cpp
View file

@ -852,7 +852,7 @@ namespace Duality {
int nargs = f.num_args();
decl_kind k = f.decl().get_decl_kind();
if(k == Implies){
res = GetLabelsRec(memo,!f.arg(0) || f.arg(1), labels, labpos);
res = GetLabelsRec(memo,f.arg(1) || !f.arg(0), labels, labpos);
goto done;
}
if(k == And) {
@ -946,7 +946,7 @@ namespace Duality {
int nargs = f.num_args();
decl_kind k = f.decl().get_decl_kind();
if(k == Implies){
ImplicantRed(memo,!f.arg(0) || f.arg(1),lits,done,truth,dont_cares);
ImplicantRed(memo,f.arg(1) || !f.arg(0) ,lits,done,truth,dont_cares);
goto done;
}
if(k == Iff){