From 9d7ee36846818f1cc49802eeec232d029deae452 Mon Sep 17 00:00:00 2001
From: Nat Karmios <nat@karmios.com>
Date: Wed, 11 Dec 2024 01:14:25 +0000
Subject: [PATCH] Fix some counterexaple production (#323)

* Fix SMT solver resets

* Fix counterexample printing
---
 .../command_line/s_interpreter_console.ml     | 44 +++++++++++++------
 .../general/g_interpreter.ml                  |  2 -
 GillianCore/smt/smt.ml                        |  2 +-
 3 files changed, 31 insertions(+), 17 deletions(-)

diff --git a/GillianCore/command_line/s_interpreter_console.ml b/GillianCore/command_line/s_interpreter_console.ml
index 06ec7585..1d4e070d 100644
--- a/GillianCore/command_line/s_interpreter_console.ml
+++ b/GillianCore/command_line/s_interpreter_console.ml
@@ -9,7 +9,8 @@ module Make
     (SState : SState.S with type init_data = ID.t)
     (S_interpreter : G_interpreter.S
                        with type annot = PC.Annot.t
-                        and type state_t = SState.t)
+                        and type state_t = SState.t
+                        and type state_err_t = SState.err_t)
     (Gil_parsing : Gil_parsing.S with type annot = PC.Annot.t) : Console.S =
 struct
   module Common_args = Common_args.Make (PC)
@@ -35,12 +36,23 @@ struct
     open ChangeTracker
 
     let counter_example res =
-      let error_state =
+      let error_state, errors =
         match res with
-        | Exec_res.RFail f -> f.error_state
+        | Exec_res.RFail { error_state; errors; _ } -> (error_state, errors)
         | _ -> failwith "Expected failure"
       in
-      let subst = SState.sat_check_f error_state [] in
+      let f =
+        errors
+        |> List.find_map (function
+             | Exec_err.EState StateErr.(EPure f) -> Some f
+             | _ -> None)
+      in
+      let fs =
+        match f with
+        | Some f -> [ Formula.Not f ]
+        | None -> []
+      in
+      let subst = SState.sat_check_f error_state fs in
       subst
 
     let run_main prog init_data =
@@ -76,11 +88,13 @@ struct
       let total_time = Sys.time () -. !start_time in
       Printf.printf "Total time (Compilation + Symbolic testing): %fs\n"
         total_time;
-      if success then (
-        Fmt.pr "%a@\n@?" (Fmt.styled `Green Fmt.string) "Success!";
-        exit 0)
-      else (
-        Fmt.pr "%a@\n@?" (Fmt.styled `Red Fmt.string) "Errors occured!";
+      if success then
+        let () = Fmt.pr "%a@\n@?" (Fmt.styled `Green Fmt.string) "Success!" in
+        exit 0
+      else
+        let () =
+          Fmt.pr "%a@\n@?" (Fmt.styled `Red Fmt.string) "Errors occured!"
+        in
         let first_error =
           List.find
             (function
@@ -94,11 +108,13 @@ struct
              ~none:(Fmt.any "Couldn't produce counter-example")
              SVal.SESubst.pp)
           counter_example;
-        Fmt.pr "Here's an example of final error state: %a@\n@?"
-          (Exec_res.pp SState.pp S_interpreter.pp_state_vt
-             S_interpreter.pp_err_t)
-          first_error;
-        exit 1)
+        let () =
+          Fmt.pr "Here's an example of final error state: %a@\n@?"
+            (Exec_res.pp SState.pp S_interpreter.pp_state_vt
+               S_interpreter.pp_err_t)
+            first_error
+        in
+        exit 1
 
     let run_incr source_files prog init_data =
       (* Only re-run program if transitive callees of main proc have changed *)
diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
index ff2e9589..43253fe7 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -533,8 +533,6 @@ struct
               Fmt.(option ~none:(any "CANNOT CREATE MODEL") ESubst.pp)
               failing_model
           in
-          if not (Exec_mode.is_biabduction_exec !Config.current_exec_mode) then
-            Printf.printf "%s" msg;
           L.normal (fun m -> m "%s" msg);
           Res_list.error_with err
 
diff --git a/GillianCore/smt/smt.ml b/GillianCore/smt/smt.ml
index 6c19626f..1e0666c9 100644
--- a/GillianCore/smt/smt.ml
+++ b/GillianCore/smt/smt.ml
@@ -988,6 +988,7 @@ let exec_sat' (fs : Formula.Set.t) (gamma : typenv) : sexp option =
           (Fmt.iter ~sep:(Fmt.any "@\n") Formula.Set.iter Formula.pp)
           fs pp_typenv gamma)
   in
+  let () = reset_solver () in
   let encoded_assertions = encode_assertions fs gamma in
   let () = if !Config.dump_smt then Dump.dump fs gamma encoded_assertions in
   let () = List.iter cmd !builtin_funcs in
@@ -1026,7 +1027,6 @@ let exec_sat' (fs : Formula.Set.t) (gamma : typenv) : sexp option =
     | Sat -> Some (get_model solver)
     | Unsat -> None
   in
-  let () = reset_solver () in
   ret
 
 let exec_sat (fs : Formula.Set.t) (gamma : typenv) : sexp option =