Use scVectorReduced when resolving array values in crucible_llvm_ve…

…rify. This fixes part of #420: The problem is fixed for crucible_llvm_verify, but does not help with crucible_jvm_verify.
GaloisInc · Apr 24, 2019 · dba90fc · dba90fc
1 parent f01563a
commit dba90fc
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs
@@ -907,7 +907,7 @@ valueToSC sym loc failMsg (Cryptol.TVSeq n cryty) (Crucible.LLVMValArray ty vals
   = do terms <- V.toList <$> traverse (valueToSC sym loc failMsg cryty) vals
        sc    <- liftIO (Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym))
        t     <- liftIO (typeToSC sc ty)
-       liftIO (scVector sc t terms)
+       liftIO (scVectorReduced sc t terms)
 
 valueToSC _ _ _ _ Crucible.LLVMValFloat{} =
   fail  "valueToSC: Real not supported"
+5 −0		prelude/Prelude.sawcore
+43 −0		src/Verifier/SAW/SharedTerm.hs