Make solver output failsafe

`cvc5` can output three different things:

1. If it found a counter-example:

```
sat
(... the model ...)
```

2. If it didn't find a counter-example:

```
unsat
(error "Cannot get model unless after a SAT or UNKNOWN response.")
```

3. If you screw things up:

```
(error "Parse Error: model_smt_prop_fp_isnan.smt2:11.59: Symbol 'zf_is_NajhghjN_D_smt' not declared as a variable")
```

Note the last one has no `sat` or `unsat`, which meant it resulted in Sail printing `Solver could not find counterexample`, which is very misleading!

This change makes it a bit safer by explicitly looking for both `sat` *and* `unsat`.

I also changed all the prints in the file to print to stdout to be consistent.

src/sail_smt_backend/smtlib.ml

@@ -690,7 +690,7 @@ let rec run frame =
 
 let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names =
   let open Printf in
-  prerr_endline ("Checking counterexample: " ^ fname);
+  print_endline ("Checking counterexample: " ^ fname);
   let in_chan = ksprintf Unix.open_process_in "%s %s" (counterexample_command !opt_auto_solver) fname in
   let lines = ref [] in
   begin
@@ -700,15 +700,15 @@ let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names
       done
     with End_of_file -> ()
   end;
-  let solver_output = List.rev !lines |> String.concat "\n" |> parse_sexps in
+  let solver_output = List.rev !lines |> String.concat "\n" in
   begin
-    match solver_output with
+    match solver_output |> parse_sexps with
     | Atom "sat" :: (List (Atom "model" :: model) | List model) :: _ ->
         let open Value in
         let open Interpreter in
         print_endline (sprintf "Solver found counterexample: %s" Util.("ok" |> green |> clear));
         let counterexample = build_counterexample args arg_ctyps arg_smt_names model in
-        List.iter (fun (id, v) -> prerr_endline ("  " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample;
+        List.iter (fun (id, v) -> print_endline ("  " ^ string_of_id id ^ " -> " ^ string_of_value v)) counterexample;
         let istate = initial_state ast env !primops in
         let annot = (Parse_ast.Unknown, Type_check.mk_tannot env bool_typ) in
         let call =
@@ -729,10 +729,13 @@ let check_counterexample ast env fname function_id args arg_ctyps arg_smt_names
               ksprintf print_endline "Replaying counterexample: %s" Util.("ok" |> green |> clear)
           | _ -> ()
         end
-    | _ ->
+    | Atom "unsat" :: _ ->
         print_endline "Solver could not find counterexample";
         print_endline "Solver output:";
-        List.iter print_endline !lines
+        print_endline solver_output
+    | _ ->
+        print_endline "Unexpected solver output:";
+        print_endline solver_output
   end;
   let status = Unix.close_process_in in_chan in
   ()