Skip to content

Commit

Permalink
Handle errors in the SMT cache file
Browse files Browse the repository at this point in the history
If we find an unexpected value in the z3_problems cache file, just
ignore the contents of the file after printing a warning.

This file being corrupt/invalid has been observed in CI
  • Loading branch information
Alasdair committed Sep 26, 2024
1 parent 65bc406 commit 8a257af
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 1 deletion.
7 changes: 6 additions & 1 deletion src/lib/constraint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,12 @@ let load_digests_err () =
| 4 ->
let solution = input_binary_int in_chan in
known_uniques := DigestMap.add digest (Some solution) !known_uniques
| _ -> assert false
| _ ->
Reporting.warn "" Parse_ast.Unknown "SMT cache file 'z3_problems' is invalid";
known_problems := DigestMap.empty;
known_uniques := DigestMap.empty;
(* Exit the loop as if we reached the end of the file *)
raise End_of_file
end;
load ()
in
Expand Down
3 changes: 3 additions & 0 deletions test/oneoff/bad_cache/bad_cache.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Warning:
SMT cache file 'z3_problems' is invalid

8 changes: 8 additions & 0 deletions test/oneoff/bad_cache/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#!/bin/sh

set -e

rm -f bad_cache.result z3_problems
echo -n -e 7fcba3a13c51ab2786c5b710e80c5f88\\x05 > z3_problems
sail --memo-z3 2> bad_cache.result || true
diff bad_cache.result bad_cache.expect

0 comments on commit 8a257af

Please sign in to comment.