From 1f6815213d6e65607e58409e65edf2d44e0da556 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 11 Apr 2020 14:16:47 -0400 Subject: [PATCH] spacer: fail with exception on quantifiers in recursive rules --- src/muz/spacer/spacer_context.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index f422f9dbc..b06aa2c00 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1676,8 +1676,17 @@ void pred_transformer::init_rule(decl2rel const& pts, datalog::rule const& rule) } TRACE("spacer_init_rule", tout << mk_pp(trans, m) << "\n";); - // allow quantifiers in init rule - SASSERT(ut_size == 0 || is_ground(trans)); + // no (universal) quantifiers in recursive rules + CTRACE("spacer", ut_size > 0 && !is_ground(trans), + tout << "Warning: quantifier in recursive rule: " << trans << "\n";); + + if (ut_size > 0 && !is_ground(trans)) { + std::stringstream stm; + stm << "spacer: quantifier in a recursive rule:\n"; + rule.display(get_context().get_datalog_context(), tout); + throw default_exception(stm.str()); + } + if (!m.is_false(trans)) { pt_rule &ptr = m_pt_rules.mk_rule(m, rule); ptr.set_trans(trans);