From d9dcbea012f5c93e88ac7096f4662b2be0fa2992 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Wed, 17 Dec 2014 17:43:06 -0800
Subject: [PATCH] WARNING: NOT SURE ABOUT THIS. For now, assume that all vars
 send to solver are finite.

---
 src/Cryptol/TypeCheck/Solver/CrySAT.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
index 60b7352e..64be96fe 100644
--- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs
+++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
@@ -299,8 +299,10 @@ declareVar Solver { .. } a =
   do done <- fmap (a `viElem`) (readIORef declared)
      unless done $
        do e  <- SMT.declare solver (smtName a)    SMT.tInt
-          _  <- SMT.declare solver (smtFinName a) SMT.tBool
-          SMT.assert solver(SMT.geq e (SMT.int 0))
+          let fin_a = smtFinName a
+          _  <- 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)
 
 -- | Add an assertion to the current context.