From d6d301c5ebe10c584798ddfd5f54128d4d83526f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Nov 2015 18:38:37 -0800 Subject: [PATCH] fix for mising handling of quantifiers in tactic. Bug #324 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/eq2bv_tactic.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index b84d5567c..7cba66a5a 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -305,14 +305,16 @@ public: m_nonfd.mark(f, true); expr* e1, *e2; if (m.is_eq(f, e1, e2)) { - if (is_fd(e1, e2)) { + if (is_fd(e1, e2) || is_fd(e2, e1)) { continue; - } - if (is_fd(e2, e1)) { - continue; - } + } } - m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + if (is_app(f)) { + m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + } + else if (is_quantifier(f)) { + m_todo.push_back(to_quantifier(f)->get_expr()); + } } }