From 8aa3a0b4f00744207305e652294b820efcbb7a68 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
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 <nbjorner@microsoft.com>
---
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];