mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

fix model generation bug reported by Saga Chaki

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-14 17:06:36 +02:00
parent 752a6b2e33
commit 72fe197bda
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "dl_mk_interp_tail_simplifier.h" #include "dl_mk_interp_tail_simplifier.h"
#include "fixedpoint_params.hpp" #include "fixedpoint_params.hpp"
#include "scoped_proof.h" #include "scoped_proof.h"
#include "model_v2_pp.h"
namespace datalog { namespace datalog {
@ -67,10 +68,16 @@ namespace datalog {
func_decl* p = m_new_funcs[i].get(); func_decl* p = m_new_funcs[i].get();
func_decl* q = m_old_funcs[i].get(); func_decl* q = m_old_funcs[i].get();
func_interp* f = model->get_func_interp(p); func_interp* f = model->get_func_interp(p);
if (!f) continue;
expr_ref body(m); expr_ref body(m);
unsigned arity_p = p->get_arity(); unsigned arity_p = p->get_arity();
unsigned arity_q = q->get_arity(); unsigned arity_q = q->get_arity();
TRACE("dl",
model_v2_pp(tout, *model);
tout << mk_pp(p, m) << "\n";
tout << mk_pp(q, m) << "\n";);
SASSERT(0 < arity_p); SASSERT(0 < arity_p);
SASSERT(f);
model->register_decl(p, f->copy()); model->register_decl(p, f->copy());
func_interp* g = alloc(func_interp, m, arity_q); func_interp* g = alloc(func_interp, m, arity_q);