Merge pull request #109 from GaloisInc/fix-fromIntMod

Fix implementation of `fromIntMod` in concrete evaluation backend.
GaloisInc · Nov 25, 2020 · 93cd7bd · 93cd7bd
2 parents 296bc6d + 2d04786
commit 93cd7bd
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/saw-core/src/Verifier/SAW/Simulator/Concrete.hs b/saw-core/src/Verifier/SAW/Simulator/Concrete.hs
@@ -254,7 +254,7 @@ constMap =
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
   , ("Prelude.toIntMod"  , toIntModOp)
-  , ("Prelude.fromIntMod", constFun (VFun force))
+  , ("Prelude.fromIntMod", fromIntModOp)
   , ("Prelude.intModEq"  , intModEqOp)
   , ("Prelude.intModAdd" , intModBinOp (+))
   , ("Prelude.intModSub" , intModBinOp (-))
@@ -320,6 +320,12 @@ toIntModOp =
   Prims.intFun "toIntModOp" $ \x -> return $
   VIntMod n (x `mod` toInteger n)
 
+fromIntModOp :: CValue
+fromIntModOp =
+  constFun $
+  Prims.intModFun "fromIntModOp" $ \x -> pure $
+  VInt x
+
 intModEqOp :: CValue
 intModEqOp =
   constFun $