Only skip assignment if we are assigned to our own initial value.

This commit is contained in:
Iavor Diatchki 2019-02-27 15:45:12 -08:00
parent 898e7bdb95
commit 1471740282

View File

@ -1221,8 +1221,7 @@ createRegUpdates regs = do
crucGenArchConstraints archFns $ do
fmap catMaybes $ forM (M.regStateMap regs & MapF.toList) $ \(Pair reg val) ->
case val of
M.Initial _ ->
return Nothing
M.Initial r | Just _ <- testEquality r reg -> return Nothing
_ -> case MapF.lookup reg idxMap of
Nothing -> fail "internal: Register is not bound."
Just idx -> Just . Pair (crucibleIndex idx) <$> valueToCrucible val