SZS status GaveUp and new line for -dkterm (#40)

* Output SZS status GaveUp when the proof search space is exhausted * Add new line at the end of -dkterm output
Deducteam · Sep 17, 2024 · d4a7041 · d4a7041
1 parent eba0f13
commit d4a7041
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/lltodk.ml b/lltodk.ml
@@ -1073,4 +1073,5 @@ let output_term oc phrases _ llp =
   fprintf oc "zenon.nnpp (%a)\n(%a)"
     print_dk_term dkgoal print_dk_term dkproof;
   if !Globals.signature_name <> "" then fprintf oc ".";
+  fprintf oc "\n";
   []
diff --git a/main.ml b/main.ml
@@ -19,6 +19,7 @@ type szs_error =
     NoSuccess
   | Unknown
   | ResourceOut
+  | GaveUp
 
 type szs_status =
     Suc of szs_success
@@ -33,6 +34,7 @@ let szs_status out (status, file) =
       | Err NoSuccess -> fprintf out "NoSuccess"
       | Err Unknown -> fprintf out "Unknown"
       | Err ResourceOut -> fprintf out "ResourceOut"
+      | Err GaveUp -> fprintf out "GaveUp"
     )
     status file
 
@@ -553,7 +555,7 @@ let main () =
   | Prove.NoProof ->
      retcode := 12;
      if not !quiet_flag then
-       print_status (Err Unknown) file
+       print_status (Err GaveUp) file
   | Prove.LimitsExceeded ->
      retcode := 13;
      if not !quiet_flag then