From 58ffffe4d4f3756381910e62c1fc4a5f169cb4c0 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 6 Apr 2014 13:01:20 -0700 Subject: [PATCH] hack to filter out Boogie axioms with large "distinct" predicates that cause legacy solver death --- src/duality/duality.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/duality/duality.h b/src/duality/duality.h index fc70ffa70..1445bc881 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -253,6 +253,10 @@ protected: } void assert_axiom(const expr &axiom){ + // HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them + if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct) + if(axiom.num_args() > 10) + return; islvr->AssertInterpolationAxiom(axiom); }