From efd0cdc740e15d6095ba57aa9b22b97cea488981 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 24 Feb 2014 14:01:51 +0000 Subject: [PATCH] bugfix for FPA --- src/tactic/fpa/qffpa_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 73faa5b50..772fd3996 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -52,7 +52,7 @@ struct is_non_qffpa_predicate { sort * s = get_sort(n); if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s))) throw found(); - if (is_uninterp(n)) + if (is_uninterp(n) && n->get_num_args() != 0) throw found(); family_id fid = s->get_family_id(); if (fid == m.get_basic_family_id()) @@ -80,7 +80,7 @@ struct is_non_qffpabv_predicate { sort * s = get_sort(n); if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s))) throw found(); - if (is_uninterp(n)) + if (is_uninterp(n) && n->get_num_args() != 0) throw found(); family_id fid = s->get_family_id(); if (fid == m.get_basic_family_id())