From a4942a80ac6d9fe0a94871a407d66e73927d3a88 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 28 Apr 2021 13:08:15 -0700 Subject: [PATCH] Make `goal_eval_unint` handle `Z n` types. Fixes #1120. --- saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 05d1495748..61dc169d6c 100644 --- 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)