From 4f7d872d591cf1f9d23807898026e4516b686dc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Jul 2014 11:21:19 +0200 Subject: [PATCH] fix model transformation bug in bit blaster rule transformer, reported by Sagar Chaki Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- src/tactic/filter_model_converter.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 90d410ab1..15d3b2f5f 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -71,7 +71,7 @@ namespace datalog { unsigned arity_p = p->get_arity(); unsigned arity_q = q->get_arity(); SASSERT(0 < arity_p); - model->register_decl(p, f); + model->register_decl(p, f->copy()); func_interp* g = alloc(func_interp, m, arity_q); if (f) { diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp index da4c71e54..ba6ee4f0d 100644 --- a/src/tactic/filter_model_converter.cpp +++ b/src/tactic/filter_model_converter.cpp @@ -43,6 +43,7 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx if (fs.is_marked(f)) continue; func_interp * fi = old_model->get_func_interp(f); + SASSERT(fi); new_model->register_decl(f, fi->copy()); } new_model->copy_usort_interps(*old_model);