Merge pull request #203 from GaloisInc/sp/crux-mir-comp

Expose Simulator.What4 helper functions for use in compositional crux-mir
GaloisInc · Apr 21, 2021 · 12a8f95 · 12a8f95
2 parents 4f93afc + 38a00f1
commit 12a8f95
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -40,6 +40,7 @@
 
 module Verifier.SAW.Simulator.What4
   ( w4Solve
+  , w4SolveBasic
   , SymFnCache
   , TypedExpr(..)
   , SValue
@@ -51,6 +52,9 @@ module Verifier.SAW.Simulator.What4
 
   , w4SimulatorEval
   , NeutralTermException(..)
+
+  , valueToSymExpr
+  , symExprToValue
   ) where