From 7f1f0415a79eb8ce7409ef605b959674d452270c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Oct 2012 14:50:39 -0700 Subject: [PATCH] fixed compilation bug Signed-off-by: Leonardo de Moura --- src/muz_qe/dl_bmc_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index a4aec2c4e..793fdd9db 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -557,7 +557,7 @@ namespace datalog { expr_ref bmc::eval_q(model_ref& model, func_decl* f, unsigned i) { func_decl_ref fn = mk_q_func_decl(f); expr_ref t(m), result(m); - t = m.mk_app(mk_q_func_decl(f), mk_q_num(i)); + t = m.mk_app(mk_q_func_decl(f).get(), mk_q_num(i)); model->eval(t, result); return result; }