remove SMT solver from RewriteStepState, use solver from arg. to evaluate (#4002)

Supplies the SMT solver from the `performRewrite` instead of a (wrong)
value from `RewriteStepState`.
We don't need the SMT solver in the `RewriteStepState` as it won't be
modified, and the old code was also setting it to `Nothing`.

Author: jberthold

booster/library/Booster/Pattern/Rewrite.hs

@@ -748,8 +748,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
     simplifyP p = withContext CtxSimplify $ do
         st <- get
         let cache = st.simplifierCache
-            smt = st.smtSolver
-        evaluatePattern def mLlvmLibrary smt cache p >>= \(res, newCache) -> do
+        evaluatePattern def mLlvmLibrary mSolver cache p >>= \(res, newCache) -> do
             updateCache newCache
             case res of
                 Right newPattern -> do
@@ -922,7 +921,6 @@ data RewriteStepsState = RewriteStepsState
     { counter :: !Natural
     , traces :: !(Seq (RewriteTrace ()))
     , simplifierCache :: SimplifierCache
-    , smtSolver :: Maybe SMT.SMTContext
     }
 
 rewriteStart :: RewriteStepsState
@@ -931,5 +929,4 @@ rewriteStart =
         { counter = 0
         , traces = mempty
         , simplifierCache = mempty
-        , smtSolver = Nothing
         }