mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

don't crash when a function doesn't have a model when converting a solver to string

Browse source
This commit is contained in:
Nuno Lopes 2023-09-18 10:16:19 +01:00
parent ff33fa355a
commit b1c52c0b16
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/converters/model_converter.cpp
View file

@ -24,7 +24,8 @@ Notes:
* Add or overwrite value in model. * Add or overwrite value in model.
*/ */
void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) { void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) {
VERIFY(e); if (!e)
return;
VERIFY(f->get_range() == e->get_sort()); VERIFY(f->get_range() == e->get_sort());
ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n"; ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n";
} }