Add test for solver crashing

boogie-org · Dec 5, 2023 · c0a1a24 · c0a1a24
1 parent ccebad6
commit c0a1a24
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/Test/prover/exitcode.bpl b/Test/prover/exitcode.bpl
@@ -0,0 +1,6 @@
+// RUN: %parallel-boogie /proverOpt:PROVER_PATH=/usr/bin/false "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure P(x: int, y: int) {
+  assert x*y == y*x;
+}
diff --git a/Test/prover/exitcode.bpl.expect b/Test/prover/exitcode.bpl.expect
@@ -0,0 +1,6 @@
+Prover error: Solver exited with code 1
+
+Advisory: P SKIPPED due to I/O exception: Broken pipe
+exitcode.bpl(4,11): Verification encountered solver exception (P)
+
+Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions