From b1c52c0b16906f4d835261b672c80905b396456a Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Mon, 18 Sep 2023 10:16:19 +0100
Subject: [PATCH] don't crash when a function doesn't have a model when
 converting a solver to string

---
 src/ast/converters/model_converter.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ast/converters/model_converter.cpp b/src/ast/converters/model_converter.cpp
index 716970cba..d053394ca 100644
--- a/src/ast/converters/model_converter.cpp
+++ b/src/ast/converters/model_converter.cpp
@@ -24,7 +24,8 @@ Notes:
  * 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) {
-    VERIFY(e);
+    if (!e)
+        return;
     VERIFY(f->get_range() == e->get_sort());
     ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n";
 }