mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

handle variables and quantifiers, fixes issue #150

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-07-06 08:34:54 -07:00
parent eeef4d29d6
commit 3fd5d0eaba
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/muz/base/hnf.cpp
View file

@ -112,6 +112,12 @@ public:
expr* n1, *n2;
while (is_forall(n)) n = to_quantifier(n)->get_expr();
if (m.is_implies(n, n1, n2) && is_predicate(n2)) {
if (is_var(n1)) {
return true;
}
if (is_quantifier(n1)) {
return false;
}
app* a1 = to_app(n1);
if (m.is_and(a1)) {
for (unsigned i = 0; i < a1->get_num_args(); ++i) {