From 8aa3a0b4f00744207305e652294b820efcbb7a68 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Oct 2012 09:11:30 -0700 Subject: [PATCH] fix compilation error under gcc reported by Arie Gurfinkel Signed-off-by: Nikolaj Bjorner --- lib/dl_bmc_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp index 13b3cdeef..a4aec2c4e 100644 --- a/lib/dl_bmc_engine.cpp +++ b/lib/dl_bmc_engine.cpp @@ -601,7 +601,7 @@ namespace datalog { rule* r = 0; unsigned i = 0; for (; i < rls.size(); ++i) { - rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level)); + rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level).get()); TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); if (m.is_true(eval_q(md, rule_i, level))) { r = rls[i];