[RyanGlScott]

This adds a logSmtInteractions flag to VerifierOptions that, when enabled, will dump each SMT solver interaction into its own file under results/. See the Haddocks for logSmtInteractions for the full details. Implementing this requires bumping the crucible submodule to bring in the changes from GaloisInc/crucible#1067, which adds support for logging offline SMT solver interactions.

This adds some information that will be needed for #23.

[RyanGlScott]

@bauer-matthews: with this patch, logging the SMT solver interactions in one of the demo programs is as simple as applying this patch:

diff --git a/copilot-verifier-demo/src/Demo1.hs b/copilot-verifier-demo/src/Demo1.hs
index f8c460b..a1ee882 100644
--- a/copilot-verifier-demo/src/Demo1.hs
+++ b/copilot-verifier-demo/src/Demo1.hs
@@ -27,6 +27,8 @@ main :: IO ()
 main = do
   interpret 6 spec
 
-  -- spec' <- reify spec
-  -- compile "demo1" spec'
-  -- verify mkDefaultCSettings [] "demo1" spec'
\ No newline at end of file
+  spec' <- reify spec
+  verifyWithOptions
+    defaultVerifierOptions{logSmtInteractions = True}
+    mkDefaultCSettings
+    [] "demo1" spec'

After running Demo1, the results can be found here:

$ ls copilot-verifier-demo/results/demo1/
crux~demo1.bc           initial-step-1-z3.smt2      transition-step-13-z3.smt2  transition-step-1-z3.smt2  transition-step-6-z3.smt2
demo1.c                 transition-step-0-z3.smt2   transition-step-14-z3.smt2  transition-step-2-z3.smt2  transition-step-7-z3.smt2
demo1.h                 transition-step-10-z3.smt2  transition-step-15-z3.smt2  transition-step-3-z3.smt2  transition-step-8-z3.smt2
demo1_types.h           transition-step-11-z3.smt2  transition-step-16-z3.smt2  transition-step-4-z3.smt2  transition-step-9-z3.smt2
initial-step-0-z3.smt2  transition-step-12-z3.smt2  transition-step-17-z3.smt2  transition-step-5-z3.smt2

If you count up all of the .smt2 files, they should total 18, the total number of proof goals.