From 27d8fa4a34468e4048ccdacd946311b6288d51b0 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 17 Aug 2017 17:18:09 -0400 Subject: [PATCH] hard-code quantifier weight to 15 With default settings, the eager threshold is 10 and lazy is 20. 15 puts us in the middle ensuring that lemmas are instantiated when UNSAT and otherwise delayed. --- src/muz/spacer/spacer_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 4968a44e4..ba4958d06 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1183,7 +1183,7 @@ void lemma::mk_expr_core() { m_body = m.mk_quantifier(true, zks.size(), sorts.c_ptr(), names.c_ptr(), - m_body, 0, symbol(m_body->get_id())); + m_body, 15, symbol(m_body->get_id())); if (m_new_pob) { add_binding(m_pob->get_binding()); }