From b7c0b16e9a21927fc9ad6c35ee13151ae83476f3 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 25 Oct 2024 16:35:43 -0700 Subject: [PATCH] move 'asScopedConst' to last rescoping strategy in practice this turns out to be the most expensive strategy to try in cases where it doesn't apply --- src/Pate/Verification/Widening.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 10b48c94..b434f87b 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -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'