From 4c8bbad8d67bca51930788392792352df209564b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Feb 2014 18:16:28 +0000 Subject: [PATCH] FPA probe bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/qffpa_tactic.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 04ffc281a..f9b7f88a1 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -57,6 +57,8 @@ struct is_non_qffpa_predicate { return; if (fid == u.get_family_id()) return; + if (is_uninterp_const(n)) + return; throw found(); } @@ -83,6 +85,8 @@ struct is_non_qffpabv_predicate { return; if (fid == fu.get_family_id() || fid == bu.get_family_id()) return; + if (is_uninterp_const(n)) + return; throw found(); }