Skip to content

Commit

Permalink
Add test case for unfinished proofs.
Browse files Browse the repository at this point in the history
Fixes #316
  • Loading branch information
robdockins committed Jul 14, 2021
1 parent 80b3825 commit 86bb800
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 0 deletions.
14 changes: 14 additions & 0 deletions intTests/test0069_unfinished/test.saw
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
enable_experimental;

let andI = core_axiom "(a b : Bool) -> EqTrue a -> EqTrue b -> EqTrue (and a b)";
let script = do { simplify (cryptol_ss()); goal_apply andI; trivial; };

b <- fresh_symbolic "b" {| Bit |};

print "The following proof should fail because the proof is incomplete.";
fails (prove_print script {{ True && b }});

print "Now we check that the 'prove' command also does the correct thing.";
r <- prove script {{ True && b }};
caseProofResult r (\_ -> fails (print "We should not get a theorem!"))
(\x -> do { prove_print z3 {{ x == () }}; return ();} );
3 changes: 3 additions & 0 deletions intTests/test0069_unfinished/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw

0 comments on commit 86bb800

Please sign in to comment.