Skip to content

Commit

Permalink
move 'asScopedConst' to last rescoping strategy
Browse files Browse the repository at this point in the history
in practice this turns out to be the most expensive
strategy to try in cases where it doesn't apply
  • Loading branch information
danmatichuk committed Oct 25, 2024
1 parent d19920a commit b7c0b16
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Pate/Verification/Widening.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1236,9 +1236,9 @@ abstractOverVars scope_pre bundle _from _to postSpec postResult = do
, ("simpleStackOffsetO", simpleStackOffset PBi.OriginalRepr se)
, ("simpleStackOffsetP", simpleStackOffset PBi.PatchedRepr se)
-- solver-based strategies now
, ("asScopedConst", asScopedConst (W4.truePred sym) se)
, ("asSimpleAssign", asSimpleAssign se)
] ++ asStackOffsetStrats
++ [ ("asScopedConst", asScopedConst (W4.truePred sym) se) ]

lift $ emitEvent (PE.ScopeAbstractionResult (PS.simPair bundle) se se')
return se'
Expand Down

0 comments on commit b7c0b16

Please sign in to comment.