mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Fixed bug in ackermannization model converter

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-14 17:46:17 +01:00
parent 8b6d7c0251
commit 5d341814d8
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ackermannization/ackr_model_converter.cpp
View file

@ -84,6 +84,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination
TRACE("ackr_model", tout << "converting constants\n";); TRACE("ackr_model", tout << "converting constants\n";);
obj_map<func_decl, func_interp*> interpretations; obj_map<func_decl, func_interp*> interpretations;
model_evaluator evaluator(*source); model_evaluator evaluator(*source);
evaluator.set_model_completion(true);
for (unsigned i = 0; i < source->get_num_constants(); i++) { for (unsigned i = 0; i < source->get_num_constants(); i++) {
func_decl * const c = source->get_constant(i); func_decl * const c = source->get_constant(i);
app * const term = info->find_term(c); app * const term = info->find_term(c);
@ -133,6 +134,11 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
args.push_back(arg_value); args.push_back(arg_value);
} }
if (fi->get_entry(args.c_ptr()) == 0) { if (fi->get_entry(args.c_ptr()) == 0) {
TRACE("ackr_model",
tout << mk_ismt2_pp(declaration, m) << " args: " << std::endl;
for (unsigned i = 0; i < args.size(); i++)
tout << mk_ismt2_pp(args.get(i), m) << std::endl;
tout << " -> " << mk_ismt2_pp(value, m) << "\n"; );
fi->insert_new_entry(args.c_ptr(), value); fi->insert_new_entry(args.c_ptr(), value);
} }
else { else {