mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix model transformation bug in bit blaster rule transformer, reported by Sagar Chaki
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d6de73a2d1
commit
4f7d872d59
|
@ -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) {
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue