Test

src/bin/common/solving_loop.ml

@@ -1458,9 +1458,12 @@ let main () =
             cmd_on_modes st [Assert; Sat; Unsat] "goal";
             let st = pop_if_post_query st in
             let st = push_before_query st in
-            let st = handle_query st id loc attrs contents in
+            let st, raised_timeout =
+              try handle_query st id loc attrs contents, false with
+              | Util.Timeout -> st, true
+            in
             let () =
-              if has_timeout st then
+              if raised_timeout || has_timeout st then
                 if Options.get_timelimit_per_goal ()
                 then begin
                   Options.Time.start ();
@@ -1475,9 +1478,12 @@ let main () =
             cmd_on_modes st [Assert; Unsat; Sat] "check-sat";
             let st = pop_if_post_query st in
             let st = push_before_query st in
-            let st = handle_solve st id contents loc attrs in
+            let st, raised_timeout =
+              try handle_solve st id contents loc attrs, false with
+              | Util.Timeout -> st, true
+            in
             let () =
-              if has_timeout st then
+              if raised_timeout || has_timeout st then
                 if Options.get_timelimit_per_goal ()
                 then begin
                   Options.Time.start ();