Skip to content

Commit d802a1c

Browse files
authored
Merge pull request #421 from GaloisInc/issue420
Use scVectorReduced when resolving array values in crucible_llvm_verify.
2 parents 19a8820 + 5e8191b commit d802a1c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/SAWScript/CrucibleOverride.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1044,7 +1044,7 @@ valueToSC sym loc failMsg (Cryptol.TVSeq n cryty) (Crucible.LLVMValArray ty vals
10441044
= do terms <- V.toList <$> traverse (valueToSC sym loc failMsg cryty) vals
10451045
sc <- liftIO $ Crucible.sawBackendSharedContext sym
10461046
t <- liftIO (typeToSC sc ty)
1047-
liftIO (scVector sc t terms)
1047+
liftIO (scVectorReduced sc t terms)
10481048

10491049
valueToSC _ _ _ _ Crucible.LLVMValFloat{} =
10501050
fail "valueToSC: Real not supported"

0 commit comments

Comments
 (0)