From 5f484c069b9342125e5ff4b6b066e5415d3ef7e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 14:15:14 +0200 Subject: [PATCH] fix distribute forall, fixes issue #138 Signed-off-by: Nikolaj Bjorner --- src/tactic/core/distribute_forall_tactic.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index 913b55174..53a1ce4ae 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -30,6 +30,10 @@ class distribute_forall_tactic : public tactic { expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { + + if (!old_q->is_forall()) { + return false; + } if (m.is_not(new_body) && m.is_or(to_app(new_body)->get_arg(0))) { // (forall X (not (or F1 ... Fn)))