Make goal_eval_unint handle Z n types.

Fixes #1120.
GaloisInc · Apr 28, 2021 · a4942a8 · a4942a8
1 parent 22dae5b
commit a4942a8
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
@@ -1193,6 +1193,9 @@ parseUninterpretedSAW sym st sc ref trm app ty =
     VIntType
       -> VInt  <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr
 
+    VIntModType n
+      -> VIntMod n <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr
+
     -- 0 width bitvector is a constant
     VVecType 0 VBoolType
       -> return $ VWord ZBV
@@ -1336,6 +1339,7 @@ mkArgTerm sc ty val =
     (_, VWord ZBV)       -> return ArgTermBVZero     -- 0-width bitvector is a constant
     (_, VWord (DBV _))   -> return ArgTermVar
     (VUnitType, VUnit)   -> return ArgTermUnit
+    (VIntModType _, VIntMod _ _) -> return ArgTermVar
 
     (VVecType _ ety, VVector vv) ->
       do vs <- traverse force (V.toList vv)