From 3fd5d0eaba7ba04d88aca6106de1360224221ec6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Jul 2015 08:34:54 -0700 Subject: [PATCH] handle variables and quantifiers, fixes issue #150 Signed-off-by: Nikolaj Bjorner --- src/muz/base/hnf.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index 58b626808..54bd727d6 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -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) {