From 2e627e78bc37003fd8070c3219088f6d2a9d7f7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 May 2015 14:55:28 -0700 Subject: [PATCH] filter tactic on proofs and cores Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/probe_arith.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index 327b074b9..e276d1792 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/src/tactic/arith/probe_arith.cpp @@ -635,7 +635,7 @@ public: static bool is_qfufnra(goal const& g) { is_non_qfufnra_functor p(g.m()); - return !test(g, p) && p.has_nonlinear(); + return !g.proofs_enabled() && !g.unsat_core_enabled() && !test(g, p) && p.has_nonlinear(); } class is_qfufnra_probe : public probe {