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

Re-simplify after applying substitution.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2014-12-17 14:29:50 -08:00
parent 8b08cca51d
commit 856e374e64
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -80,7 +80,9 @@ checkDefined s uniVars props0 = withScope s (go Map.empty [] props0)
let (g,p) = smtpOther ct
in case apSubst su p of
Nothing -> ct
Just p' -> (prepareProp p') { smtpOther = (g,p') }
Just p' ->
let p2 = crySimpPropExpr p'
in (prepareProp p2) { smtpOther = (g,p2) }
updNotDone su (g,p) =
case apSubst su p of