Make iget_answer recursively call check_formula

smtsolver.ml

@@ -728,10 +728,9 @@ let rec iget_answer_x chn input timeout =
       with _ -> last_z3_sat_type
     else last_z3_sat_type
   in
-  (* match st with
-   * | Unknown -> let input = "(reset)\n" ^ input in let () = print_endline ("[smtsolver.ml] Z3 outputted unknown, retry with (reset) instead of (push) and (pop), new input:\n" ^ input) in check_formula input timeout
-   * | _ -> { original_output_text = output; sat_result =  st; } *)
-  { original_output_text = output; sat_result =  st; }
+  match st with
+  | Unknown -> let input = "(reset)\n" ^ input in let () = print_endline ("[smtsolver.ml] Z3 outputted unknown, retry with (reset) instead of (push) and (pop), new input:\n" ^ input) in check_formula input timeout
+  | _ -> { original_output_text = output; sat_result =  st; }
 
 and iget_answer chn input timeout =
   Debug.no_1 "Z3.iget_answer" idf (fun o -> pr_list idf o.original_output_text)