return string model from solve()

src/halmos/__main__.py

@@ -975,10 +975,6 @@ class GenModelArgs:
     dump_dirname: str | None = None
 
 
-def copy_model(model: ModelRef) -> dict:
-    return {decl: model[decl] for decl in model}
-
-
 def parse_unsat_core(output) -> list | None:
     # parsing example:
     #   unsat
@@ -1072,7 +1068,7 @@ def solve(
             result = solver.check(*ids)
         else:
             result = solver.check()
-        model = copy_model(solver.model()) if result == sat else None
+        model = to_str_model(solver.model(), args.print_full_model) if result == sat else None
         unsat_core = (
             [str(core) for core in solver.unsat_core()]
             if args.cache_solver and result == unsat
@@ -1171,7 +1167,6 @@ def package_result(
                 model = f"see {model}"
             else:
                 is_valid = is_model_valid(model)
-                model = to_str_model(model, args.print_full_model)
 
         return ModelWithContext(model, is_valid, idx, result, None)
 
@@ -1201,7 +1196,7 @@ def is_model_valid(model: AnyModel) -> bool:
 def to_str_model(model: ModelRef, print_full_model: bool) -> StrModel:
     def select(var):
         name = str(var)
-        return name.startswith("p_") or name.startswith("halmos_")
+        return name.startswith("p_") or name.startswith("halmos_") or name.startswith("f_evm_")
 
     select_model = filter(select, model) if not print_full_model else model
     return {str(decl): stringify(str(decl), model[decl]) for decl in select_model}