diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml
index d313b4e..ca8e934 100644
--- a/.github/workflows/docker-image.yml
+++ b/.github/workflows/docker-image.yml
@@ -32,8 +32,9 @@ jobs:
           set +e
           racket ./picus.rkt ${{ matrix.param }} | tee result.out
           code=$?
-          if [ $code -ne 0 ] && [ $code -ne 9 ]; then
-            exit $code
+          if [ $code -ne 9 ]; then
+            echo "original exit code: $code"
+            exit 1
           fi
         shell: bash # this ensures that pipefail is set
       - name: test expected result
@@ -55,8 +56,9 @@ jobs:
           set +e
           racket ./picus.rkt --wtns . ./benchmarks/circomlib-cff5ab6/Decoder@multiplexer.circom
           code=$?
-          if [ $code -ne 0 ] && [ $code -ne 9 ]; then
-            exit $code
+          if [ $code -ne 9 ]; then
+            echo "original exit code: $code"
+            exit 1
           fi
         shell: bash # this ensures that pipefail is set
       - name: test expected result
diff --git a/picus.rkt b/picus.rkt
index 5a03dc6..4823951 100644
--- a/picus.rkt
+++ b/picus.rkt
@@ -299,6 +299,9 @@
   (when (empty? info)
     (picus:log-main "    no ~a" heading)))
 
+(when arg-clean?
+  (clean-tmpdir!))
+
 (match res
   ['unsafe
    (picus:log-main "The circuit is underconstrained")
@@ -315,12 +318,10 @@
    (when arg-wtns
      (parameterize ([current-directory arg-wtns])
        (gen-witness raw-res-info r0)))
-
-   (picus:exit exit-code:issues)]
+   (picus:exit exit-code:unsafe)]
   ['safe
-   (picus:log-main "The circuit is properly constrained")]
+   (picus:log-main "The circuit is properly constrained")
+   (picus:exit exit-code:safe)]
   ['unknown
-   (picus:log-main "Cannot determine whether the circuit is properly constrained")])
-
-(when arg-clean?
-  (clean-tmpdir!))))
+   (picus:log-main "Cannot determine whether the circuit is properly constrained")
+   (picus:exit exit-code:unknown)])))
diff --git a/picus/exit.rkt b/picus/exit.rkt
index 2506c29..dc9c270 100644
--- a/picus/exit.rkt
+++ b/picus/exit.rkt
@@ -1,8 +1,9 @@
 #lang racket/base
 
 (provide picus:exit
-         exit-code:success
-         exit-code:issues
+         exit-code:safe
+         exit-code:unsafe
+         exit-code:unknown
          exit-code:tool-failure
          exit-code:tool-error
          exit-code:user-error
@@ -19,11 +20,14 @@
   (sleep 0.1)
   (exit code))
 
-;; exits normally
-(define exit-code:success 0)
+;; exits with the unknown status
+(define exit-code:unknown 0)
+
+;; exits with a guarantee
+(define exit-code:safe 8)
 
 ;; exits with issues
-(define exit-code:issues 9)
+(define exit-code:unsafe 9)
 
 ;; exits with tool failure (e.g., uncaught exception)
 (define exit-code:tool-failure 1)
diff --git a/picus/framework.rkt b/picus/framework.rkt
index 1634df5..19b1156 100644
--- a/picus/framework.rkt
+++ b/picus/framework.rkt
@@ -95,8 +95,7 @@
       (with-handlers ([exn:fail? (λ (e)
                                    (picus:log-exception e)
                                    (picus:exit exit-code:tool-failure))])
-        (proc))
-      (picus:exit exit-code:success))
+        (proc)))
     #:logger picus-logger
     'debug ; debug is the lowest level of logging, so this intercepts everything
     #f))
@@ -106,11 +105,14 @@
 ;;                   #:json? boolean?
 ;;                   #:truncate? boolean?
 ;;                   #:level string?
-;;                   (-> any)
+;;                   (-> never/c)
 ;;                   ->
 ;;                   never
 ;; Note that if #:err is the same as #:out, then 'out should be given.
 ;; so that we avoid (potentially) opening the same file twice.
+;;
+;; The proc positional argument must never return. Instead, it should exit with
+;; picus:exit.
 (define (with-framework
           #:json? json?
           #:truncate? truncate?
diff --git a/tests/circomlib-test.rkt b/tests/circomlib-test.rkt
index e9346c0..73f25ea 100644
--- a/tests/circomlib-test.rkt
+++ b/tests/circomlib-test.rkt
@@ -89,8 +89,9 @@
       [_ (printf "TIMEOUT\n")])
 
     (match expected
-      [(or 'safe 'unknown) (check-equal? ret-code exit-code:success)]
-      ['unsafe (check-equal? ret-code exit-code:issues)]
+      ['safe (check-equal? ret-code exit-code:safe)]
+      ['unknown (check-equal? ret-code exit-code:unknown)]
+      ['unsafe (check-equal? ret-code exit-code:unsafe)]
       ['timeout (check-false ret-code)])
 
     (match expected
diff --git a/tests/framework-test.rkt b/tests/framework-test.rkt
index 3d231f1..321779a 100644
--- a/tests/framework-test.rkt
+++ b/tests/framework-test.rkt
@@ -38,10 +38,11 @@
      #:level "ERROR"
      (λ ()
        (picus:log-error "foo")
-       (picus:log-info "bar")))
+       (picus:log-info "bar")
+       (picus:exit exit-code:safe)))
 
    #:check-status code
-   (check-equal? code 0)
+   (check-equal? code exit-code:safe)
 
    #:check out err
    (check-equal? out "")
@@ -56,10 +57,11 @@
      #:level "INFO"
      (λ ()
        (picus:log-error "foo")
-       (picus:log-info "bar")))
+       (picus:log-info "bar")
+       (picus:exit exit-code:safe)))
 
    #:check-status code
-   (check-equal? code 0)
+   (check-equal? code exit-code:safe)
 
    #:check out err
    (check-regexp-match #px"bar" out)
@@ -74,10 +76,11 @@
      #:level #f
      (λ ()
        (picus:log-error "foo")
-       (picus:log-info "bar")))
+       (picus:log-info "bar")
+       (picus:exit exit-code:safe)))
 
    #:check-status code
-   (check-equal? code 0)
+   (check-equal? code exit-code:safe)
 
    #:check out err
    (check-equal? err "")
@@ -86,21 +89,21 @@
 
    ;; log-error
    (define json-err (first jsons))
-   (check-regexp-match #px"framework-test\\.rkt:76:7" (hash-ref json-err 'caller))
+   (check-regexp-match #px"framework-test\\.rkt" (hash-ref json-err 'caller))
    (check-equal? (hash-ref json-err 'level) "ERROR")
    (check-equal? (hash-ref json-err 'msg) "foo")
 
    ;; log-info
    (define json-info (second jsons))
-   (check-regexp-match #px"framework-test\\.rkt:77:7" (hash-ref json-info 'caller))
+   (check-regexp-match #px"framework-test\\.rkt" (hash-ref json-info 'caller))
    (check-equal? (hash-ref json-info 'level) "INFO")
    (check-equal? (hash-ref json-info 'msg) "bar")
 
    ;; exit-info
    (define json-exit (third jsons))
-   (check-regexp-match #px"exit\\.rkt:18:2" (hash-ref json-exit 'caller))
+   (check-regexp-match #px"exit\\.rkt" (hash-ref json-exit 'caller))
    (check-equal? (hash-ref json-exit 'level) "INFO")
-   (check-equal? (hash-ref json-exit 'msg) "Exiting Picus with the code 0")))
+   (check-equal? (hash-ref json-exit 'msg) "Exiting Picus with the code 8")))
 
 (test-case "test exit code"
   (run-test
@@ -112,7 +115,8 @@
      (λ ()
        (picus:log-error "foo")
        (picus:tool-error "bad")
-       (picus:log-info "bar")))
+       (picus:log-info "bar")
+       (picus:exit exit-code:safe)))
 
    #:check-status code
    (check-equal? code exit-code:tool-error)
@@ -121,3 +125,22 @@
    ;; control not reached log-info
    (check-false (regexp-match #px"bar" out))
    (check-regexp-match #px"foo" err)))
+
+(test-case "test unexpected exception"
+  (run-test
+   #:setup
+   (with-framework
+     #:json? #f
+     #:truncate? #f
+     #:level "INFO"
+     (λ ()
+       (/ 1 0)
+       (picus:log-info "bar")
+       (picus:exit exit-code:safe)))
+
+   #:check-status code
+   (check-equal? code exit-code:tool-failure)
+
+   #:check out err
+   ;; control not reached log-info
+   (check-false (regexp-match #px"bar" out))))