mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

duality fix

Browse source
This commit is contained in:
Ken McMillan 2014-04-01 17:50:48 -07:00
parent 278d619521
commit 4671c1be41
1 changed files with 4172 additions and 4172 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/duality/duality_rpfp.cpp
View file

@ -579,7 +579,7 @@ namespace Duality {
args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall); args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall);
return SimplifyAndOr(args, body.decl().get_decl_kind() == And); return SimplifyAndOr(args, body.decl().get_decl_kind() == And);
} }
else if(body.decl().get_decl_kind() == is_forall ? And : Or){ // quantifier distributes else if(body.decl().get_decl_kind() == (is_forall ? And : Or)){ // quantifier distributes
return PushQuantifier(t,body,is_forall); // may distribute partially return PushQuantifier(t,body,is_forall); // may distribute partially
} }
else if(body.decl().get_decl_kind() == Not){ else if(body.decl().get_decl_kind() == Not){