From f1317962f62073b21f398cb4046b019c278c9f28 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 10:09:56 -0500 Subject: [PATCH 1/4] Remove redundant import --- what4/src/What4/Protocol/SMTLib2.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index 16b1a60b..a3820cd1 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -101,7 +101,7 @@ import Control.Monad.Fail( MonadFail ) import Control.Applicative import Control.Exception -import Control.Monad (forM, forM_, replicateM_, unless, when) +import Control.Monad (forM, replicateM_, unless, when) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Except (MonadError(..), ExceptT, runExceptT) import Control.Monad.Reader (MonadReader(..), ReaderT(..), asks) From 72dd5ff5741caee5a40ca5f5791201a54f6064b7 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 1 Mar 2024 10:08:25 -0500 Subject: [PATCH 2/4] Guard mux-pushing simplifications behind option --- what4/src/What4/Expr.hs | 1 + what4/src/What4/Expr/Builder.hs | 190 +++++++++++++++++++++----------- what4/test/AdapterTest.hs | 40 +++++++ 3 files changed, 169 insertions(+), 62 deletions(-) diff --git a/what4/src/What4/Expr.hs b/what4/src/What4/Expr.hs index ff97fcfd..94a5ca7b 100644 --- a/what4/src/What4/Expr.hs +++ b/what4/src/What4/Expr.hs @@ -20,6 +20,7 @@ module What4.Expr , curProgramLoc , unaryThreshold , cacheStartSize + , pushMuxOps , exprBuilderSplitConfig , exprBuilderFreshConfig , EmptyExprBuilderState(..) diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 3bc99057..5f7440f3 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -58,6 +58,7 @@ module What4.Expr.Builder , sbNonceExpr , curProgramLoc , unaryThreshold + , pushMuxOps , cacheStartSize , userState , exprCounter @@ -76,6 +77,7 @@ module What4.Expr.Builder -- * configuration options , unaryThresholdOption , cacheStartSizeOption + , pushMuxOpsOption , cacheTerms -- * Expr @@ -374,6 +376,12 @@ data ExprBuilder t (st :: Type -> Type) (fs :: Type) -- | The starting size when building a new cache , sbCacheStartSize :: !(CFG.OptionSetting BaseIntegerType) + -- | If enabled, push certain 'ExprBuilder' operations (e.g., @zext@) + -- down to the branches of @ite@ expressions. In some (but not all) + -- circumstances, this can result in operations that are easier for + -- SMT solvers to reason about. + , sbPushMuxOps :: !(CFG.OptionSetting BaseBoolType) + -- | Counter to generate new unique identifiers for elements and functions. , sbExprCounter :: !(NonceGenerator IO t) @@ -421,6 +429,9 @@ unaryThreshold = to sbUnaryThreshold cacheStartSize :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType) cacheStartSize = to sbCacheStartSize +pushMuxOps :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType) +pushMuxOps = to sbPushMuxOps + -- | Return a new expr builder where the configuration object has -- been "split" using the @splitConfig@ operation. -- The returned sym will share any preexisting options with the @@ -456,9 +467,11 @@ exprBuilderFreshConfig sym = cfg <- CFG.initialConfig 0 [ unaryThresholdDesc , cacheStartSizeDesc + , pushMuxOpsDesc ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg + pushMuxOpsStartSetting <- CFG.getOptionSetting pushMuxOpsOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0 @@ -466,6 +479,7 @@ exprBuilderFreshConfig sym = , sbFloatReduce = True , sbUnaryThreshold = unarySetting , sbCacheStartSize = cacheStartSetting + , sbPushMuxOps = pushMuxOpsStartSetting , sbProgramLoc = loc_ref , sbCurAllocator = storage_ref , sbNonLinearOps = nonLinearOps @@ -650,6 +664,19 @@ unaryThresholdDesc = CFG.mkOpt unaryThresholdOption sty help (Just (ConcreteInte where sty = CFG.integerWithMinOptSty (CFG.Inclusive 0) help = Just "Maximum number of values in unary bitvector encoding." +------------------------------------------------------------------------ +-- Configuration option for controlling whether to push certain ExprBuilder +-- operations (e.g., @zext@) down to the branches of @ite@ expressions. + +-- | TODO RGS: Docs +pushMuxOpsOption :: CFG.ConfigOption BaseBoolType +pushMuxOpsOption = CFG.configOption BaseBoolRepr "backend.push_mux_ops" + +-- | TODO RGS: Docs +pushMuxOpsDesc :: CFG.ConfigDesc +pushMuxOpsDesc = CFG.mkOpt pushMuxOpsOption sty help (Just (ConcreteBool False)) + where sty = CFG.boolOptSty + help = Just "Maximum number of values in unary bitvector encoding." newExprBuilder :: @@ -678,9 +705,11 @@ newExprBuilder floatMode st gen = do cfg <- CFG.initialConfig 0 [ unaryThresholdDesc , cacheStartSizeDesc + , pushMuxOpsDesc ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg + pushMuxOpsStartSetting <- CFG.getOptionSetting pushMuxOpsOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0 @@ -691,6 +720,7 @@ newExprBuilder floatMode st gen = do , sbFloatReduce = True , sbUnaryThreshold = unarySetting , sbCacheStartSize = cacheStartSetting + , sbPushMuxOps = pushMuxOpsStartSetting , sbProgramLoc = loc_ref , sbExprCounter = gen , sbCurAllocator = storage_ref @@ -2913,17 +2943,20 @@ instance IsExprBuilder (ExprBuilder t st fs) where Just LeqProof <- return $ isPosNat w bvUnary sym $ UnaryBV.uext u w - | Just (BaseIte _ _ c a b) <- asApp x - , Just a_bv <- asBV a - , Just b_bv <- asBV b = do - Just LeqProof <- return $ isPosNat w - a' <- bvLit sym w $ BV.zext w a_bv - b' <- bvLit sym w $ BV.zext w b_bv - bvIte sym c a' b' - | otherwise = do - Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w - sbMakeExpr sym $ BVZext w x + pmo <- CFG.getOpt (sbPushMuxOps sym) + if | pmo + , Just (BaseIte _ _ c a b) <- asApp x + , Just a_bv <- asBV a + , Just b_bv <- asBV b -> do + Just LeqProof <- return $ isPosNat w + a' <- bvLit sym w $ BV.zext w a_bv + b' <- bvLit sym w $ BV.zext w b_bv + bvIte sym c a' b' + + | otherwise -> do + Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w + sbMakeExpr sym $ BVZext w x bvSext sym w x | Just xv <- asBV x = do @@ -2944,17 +2977,20 @@ instance IsExprBuilder (ExprBuilder t st fs) where Just LeqProof <- return $ isPosNat w bvUnary sym $ UnaryBV.sext u w - | Just (BaseIte _ _ c a b) <- asApp x - , Just a_bv <- asBV a - , Just b_bv <- asBV b = do - Just LeqProof <- return $ isPosNat w - a' <- bvLit sym w $ BV.sext (bvWidth x) w a_bv - b' <- bvLit sym w $ BV.sext (bvWidth x) w b_bv - bvIte sym c a' b' - | otherwise = do - Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w - sbMakeExpr sym (BVSext w x) + pmo <- CFG.getOpt (sbPushMuxOps sym) + if | pmo + , Just (BaseIte _ _ c a b) <- asApp x + , Just a_bv <- asBV a + , Just b_bv <- asBV b -> do + Just LeqProof <- return $ isPosNat w + a' <- bvLit sym w $ BV.sext (bvWidth x) w a_bv + b' <- bvLit sym w $ BV.sext (bvWidth x) w b_bv + bvIte sym c a' b' + + | otherwise -> do + Just LeqProof <- return $ testLeq (knownNat :: NatRepr 1) w + sbMakeExpr sym (BVSext w x) bvXorBits sym x y | x == y = bvLit sym (bvWidth x) (BV.zero (bvWidth x)) -- special case: x `xor` x = 0 @@ -2965,22 +3001,6 @@ instance IsExprBuilder (ExprBuilder t st fs) where bvAndBits sym x y | x == y = return x -- Special case: idempotency of and - | Just (BaseIte _ _ c a b) <- asApp x - , Just a_bv <- asBV a - , Just b_bv <- asBV b - , Just y_bv <- asBV y = do - a' <- bvLit sym (bvWidth x) $ BV.and a_bv y_bv - b' <- bvLit sym (bvWidth x) $ BV.and b_bv y_bv - bvIte sym c a' b' - - | Just (BaseIte _ _ c a b) <- asApp y - , Just a_bv <- asBV a - , Just b_bv <- asBV b - , Just x_bv <- asBV x = do - a' <- bvLit sym (bvWidth x) $ BV.and x_bv a_bv - b' <- bvLit sym (bvWidth x) $ BV.and x_bv b_bv - bvIte sym c a' b' - | Just (BVOrBits _ bs) <- asApp x , bvOrContains y bs = return y -- absorption law @@ -2990,8 +3010,28 @@ instance IsExprBuilder (ExprBuilder t st fs) where = return x -- absorption law | otherwise - = let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x) - in semiRingMul sym sr x y + = do pmo <- CFG.getOpt (sbPushMuxOps sym) + if | pmo + , Just (BaseIte _ _ c a b) <- asApp x + , Just a_bv <- asBV a + , Just b_bv <- asBV b + , Just y_bv <- asBV y -> do + a' <- bvLit sym (bvWidth x) $ BV.and a_bv y_bv + b' <- bvLit sym (bvWidth x) $ BV.and b_bv y_bv + bvIte sym c a' b' + + | pmo + , Just (BaseIte _ _ c a b) <- asApp y + , Just a_bv <- asBV a + , Just b_bv <- asBV b + , Just x_bv <- asBV x -> do + a' <- bvLit sym (bvWidth x) $ BV.and x_bv a_bv + b' <- bvLit sym (bvWidth x) $ BV.and x_bv b_bv + bvIte sym c a' b' + + | otherwise + -> let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x) + in semiRingMul sym sr x y -- XOR by the all-1 constant of the bitwise semiring. -- This is equivalant to negation @@ -2999,16 +3039,18 @@ instance IsExprBuilder (ExprBuilder t st fs) where | Just xv <- asBV x = bvLit sym (bvWidth x) $ xv `BV.xor` (BV.maxUnsigned (bvWidth x)) - | Just (BaseIte _ _ c a b) <- asApp x - , Just a_bv <- asBV a - , Just b_bv <- asBV b = do - a' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) a_bv - b' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) b_bv - bvIte sym c a' b' - | otherwise - = let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)) - in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x)) + = do pmo <- CFG.getOpt (sbPushMuxOps sym) + if | pmo + , Just (BaseIte _ _ c a b) <- asApp x + , Just a_bv <- asBV a + , Just b_bv <- asBV b -> do + a' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) a_bv + b' <- bvLit sym (bvWidth x) $ BV.complement (bvWidth x) b_bv + bvIte sym c a' b' + | otherwise -> + let sr = (SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)) + in semiRingSum sym $ WSum.addConstant sr (asWeightedSum sr x) (BV.maxUnsigned (bvWidth x)) bvOrBits sym x y = case (asBV x, asBV y) of @@ -3085,20 +3127,23 @@ instance IsExprBuilder (ExprBuilder t st fs) where bvNeg sym x | Just xv <- asBV x = bvLit sym (bvWidth x) (BV.negate (bvWidth x) xv) - | Just (BaseIte _ _ c a b) <- asApp x - , Just a_bv <- asBV a - , Just b_bv <- asBV b = do - a' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) a_bv - b' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) b_bv - bvIte sym c a' b' - | otherwise = - do ut <- CFG.getOpt (sbUnaryThreshold sym) - let ?unaryThreshold = fromInteger ut - sbTryUnaryTerm sym - (do ux <- asUnaryBV sym x - Just (UnaryBV.neg sym ux)) - (do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x) - scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x) + | otherwise = do + pmo <- CFG.getOpt (sbPushMuxOps sym) + if | pmo + , Just (BaseIte _ _ c a b) <- asApp x + , Just a_bv <- asBV a + , Just b_bv <- asBV b -> do + a' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) a_bv + b' <- bvLit sym (bvWidth x) $ BV.negate (bvWidth x) b_bv + bvIte sym c a' b' + | otherwise -> do + ut <- CFG.getOpt (sbUnaryThreshold sym) + let ?unaryThreshold = fromInteger ut + sbTryUnaryTerm sym + (do ux <- asUnaryBV sym x + Just (UnaryBV.neg sym ux)) + (do let sr = SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x) + scalarMul sym sr (BV.mkBV (bvWidth x) (-1)) x) bvIsNonzero sym x | Just (BaseIte _ _ p t f) <- asApp x @@ -3391,7 +3436,28 @@ instance IsExprBuilder (ExprBuilder t st fs) where else sbMakeExpr sym $ ArrayMap idx_tps baseRepr new_map def_map - arrayIte sym p x y = mkIte sym p x y + arrayIte sym p x y = do + pmo <- CFG.getOpt (sbPushMuxOps sym) + if -- Extract all concrete updates out. + | not pmo + , ArrayMapView mx x' <- viewArrayMap x + , ArrayMapView my y' <- viewArrayMap y + , not (AUM.null mx) || not (AUM.null my) -> do + case exprType x of + BaseArrayRepr idxRepr bRepr -> do + let both_fn _ u v = baseTypeIte sym p u v + left_fn idx u = do + v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx + both_fn idx u v + right_fn idx v = do + u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx + both_fn idx u v + mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my + z' <- arrayIte sym p x' y' + + sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z' + + | otherwise -> mkIte sym p x y arrayEq sym x y | x == y = diff --git a/what4/test/AdapterTest.hs b/what4/test/AdapterTest.hs index 9cec1d90..842c07c5 100644 --- a/what4/test/AdapterTest.hs +++ b/what4/test/AdapterTest.hs @@ -33,6 +33,7 @@ import Data.Parameterized.Some import What4.Config import What4.Expr +import What4.Expr.Builder ( asApp, pushMuxOpsOption ) import What4.Interface import What4.Protocol.SMTLib2.Response ( strictSMTParsing ) import What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) ) @@ -86,6 +87,7 @@ mkConfigTests adapters = [ testGroup "deprecated configs" (deprecatedConfigTests adapters) , testGroup "strict parsing config" (strictParseConfigTests adapters) + , testGroup "push mux ops config" (pushMuxOpsConfigTests adapters) ] where wantOptSetFailure withText res = case res of @@ -223,6 +225,44 @@ mkConfigTests adapters = ] in fmap mkPCTest adaptrs + pushMuxOpsConfigTests adaptrs = + let -- A basic test that ensures that pushMuxOps actually takes effect + -- when enabled or disabled. + mkPushZextMuxTest :: + forall a. + Bool -> + (forall t. Expr t (BaseBVType 64) -> IO a) -> + IO a + mkPushZextMuxTest pushMuxOpsVal k = + withAdapters adaptrs $ \sym -> do + pmo <- getOptionSetting pushMuxOpsOption (getConfiguration sym) + show <$> setOpt pmo pushMuxOpsVal >>= (@?= "[]") + let w = knownNat @32 + a <- bvLit sym w $ mkBV w 27 + b <- bvLit sym w $ mkBV w 42 + c <- freshConstant sym (safeSymbol "c") BaseBoolRepr + ite <- bvIte sym c a b + zextIte <- bvZext sym (knownNat @64) ite + k zextIte + in [ testCase "enable pushMuxOps" $ + mkPushZextMuxTest True $ \zextIte -> + case asApp zextIte of + Just (BaseIte {}) -> pure () + _ -> assertFailure $ unlines + [ "zext not pushed down through ite" + , show $ printSymExpr zextIte + ] + + , testCase "disable pushMuxOps" $ + mkPushZextMuxTest False $ \zextIte -> + case asApp zextIte of + Just (BVZext {}) -> pure () + _ -> assertFailure $ unlines + [ "zext should be at the head of the application" + , show $ printSymExpr zextIte + ] + ] + deprecatedConfigTests adaptrs = [ From 512eca66373a900be1175c1e06aed4041bcf6f54 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 13 May 2024 16:41:55 -0400 Subject: [PATCH 3/4] Document pushMuxOps in Haddocks and CHANGELOG --- what4/CHANGES.md | 5 +++++ what4/src/What4/Expr/Builder.hs | 9 +++++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/what4/CHANGES.md b/what4/CHANGES.md index ef38fca8..681b2cce 100644 --- a/what4/CHANGES.md +++ b/what4/CHANGES.md @@ -2,6 +2,11 @@ * Add support for the `bitwuzla` SMT solver. +* Add `pushMuxOps` and `pushMuxOpsOption`. If this option is enabled, What4 will + push certain `ExprBuilder` operations (e.g., `zext`) down to the branches of + `ite` expressions. In some (but not all) circumstances, this can result in + operations that are easier for SMT solvers to reason about. + # 1.5.1 (October 2023) * Require building with `versions >= 6.0.2`. diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 9e019d0d..52f50b4d 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -668,11 +668,16 @@ unaryThresholdDesc = CFG.mkOpt unaryThresholdOption sty help (Just (ConcreteInte -- Configuration option for controlling whether to push certain ExprBuilder -- operations (e.g., @zext@) down to the branches of @ite@ expressions. --- | TODO RGS: Docs +-- | If this option enabled, push certain 'ExprBuilder' operations (e.g., +-- @zext@) down to the branches of @ite@ expressions. In some (but not all) +-- circumstances, this can result in operations that are easier for SMT solvers +-- to reason about. +-- +-- This option is named \"backend.push_mux_ops\". pushMuxOpsOption :: CFG.ConfigOption BaseBoolType pushMuxOpsOption = CFG.configOption BaseBoolRepr "backend.push_mux_ops" --- | TODO RGS: Docs +-- | The 'CFG.ConfigDesc' for 'pushMuxOpsOption'. pushMuxOpsDesc :: CFG.ConfigDesc pushMuxOpsDesc = CFG.mkOpt pushMuxOpsOption sty help (Just (ConcreteBool False)) where sty = CFG.boolOptSty From fa36855a8c92b0dc6380d889ff1f7807fd309ded Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 14 May 2024 06:52:06 -0400 Subject: [PATCH 4/4] Review comments --- what4/src/What4/Expr/Builder.hs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 52f50b4d..dc39a467 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -471,7 +471,7 @@ exprBuilderFreshConfig sym = ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg - pushMuxOpsStartSetting <- CFG.getOptionSetting pushMuxOpsOption cfg + pushMuxOpsSetting <- CFG.getOptionSetting pushMuxOpsOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0 @@ -479,7 +479,7 @@ exprBuilderFreshConfig sym = , sbFloatReduce = True , sbUnaryThreshold = unarySetting , sbCacheStartSize = cacheStartSetting - , sbPushMuxOps = pushMuxOpsStartSetting + , sbPushMuxOps = pushMuxOpsSetting , sbProgramLoc = loc_ref , sbCurAllocator = storage_ref , sbNonLinearOps = nonLinearOps @@ -671,7 +671,9 @@ unaryThresholdDesc = CFG.mkOpt unaryThresholdOption sty help (Just (ConcreteInte -- | If this option enabled, push certain 'ExprBuilder' operations (e.g., -- @zext@) down to the branches of @ite@ expressions. In some (but not all) -- circumstances, this can result in operations that are easier for SMT solvers --- to reason about. +-- to reason about. The expressions that may be pushed down are determined on a +-- case-by-case basis in the 'IsExprBuilder' instance for 'ExprBuilder', but +-- this control applies to all such push-down checks. -- -- This option is named \"backend.push_mux_ops\". pushMuxOpsOption :: CFG.ConfigOption BaseBoolType @@ -681,8 +683,9 @@ pushMuxOpsOption = CFG.configOption BaseBoolRepr "backend.push_mux_ops" pushMuxOpsDesc :: CFG.ConfigDesc pushMuxOpsDesc = CFG.mkOpt pushMuxOpsOption sty help (Just (ConcreteBool False)) where sty = CFG.boolOptSty - help = Just "Maximum number of values in unary bitvector encoding." - + help = Just $ + "If this option enabled, push certain ExprBuilder operations " <> + "(e.g., zext) down to the branches of ite expressions." newExprBuilder :: FloatModeRepr fm @@ -714,7 +717,7 @@ newExprBuilder floatMode st gen = do ] unarySetting <- CFG.getOptionSetting unaryThresholdOption cfg cacheStartSetting <- CFG.getOptionSetting cacheStartSizeOption cfg - pushMuxOpsStartSetting <- CFG.getOptionSetting pushMuxOpsOption cfg + pushMuxOpsSetting <- CFG.getOptionSetting pushMuxOpsOption cfg CFG.extendConfig [cacheOptDesc gen storage_ref cacheStartSetting] cfg nonLinearOps <- newIORef 0 @@ -725,7 +728,7 @@ newExprBuilder floatMode st gen = do , sbFloatReduce = True , sbUnaryThreshold = unarySetting , sbCacheStartSize = cacheStartSetting - , sbPushMuxOps = pushMuxOpsStartSetting + , sbPushMuxOps = pushMuxOpsSetting , sbProgramLoc = loc_ref , sbExprCounter = gen , sbCurAllocator = storage_ref