GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-18 13:31:50 +03:00
Code Issues Projects Releases Wiki Activity

WARNING: NOT SURE ABOUT THIS. For now, assume that all vars send to solver are finite.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2014-12-17 17:43:06 -08:00
parent a23d294b1c
commit d9dcbea012
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Cryptol/TypeCheck/Solver/CrySAT.hs
View File

@ -299,8 +299,10 @@ declareVar Solver { .. } a =
do done <- fmap (a `viElem`) (readIORef declared) do done <- fmap (a `viElem`) (readIORef declared)
unless done $ unless done $
do e <- SMT.declare solver (smtName a) SMT.tInt do e <- SMT.declare solver (smtName a) SMT.tInt
_ <- SMT.declare solver (smtFinName a) SMT.tBool let fin_a = smtFinName a
SMT.assert solver(SMT.geq e (SMT.int 0)) _ <- SMT.declare solver fin_a SMT.tBool
SMT.assert solver (SMT.geq e (SMT.int 0))
SMT.assert solver (SMT.const fin_a) -- HMM ???
modifyIORef' declared (viInsert a) modifyIORef' declared (viInsert a)
-- | Add an assertion to the current context. -- | Add an assertion to the current context.