107-smart-ite: solveOptimized clears all additional assertions

src/Language/Hasmtlib/Type/Solver.hs

@@ -313,9 +313,9 @@ solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)
   -> Maybe (Expr t -> Expr t)
   -> Maybe (Solution -> IO ())
   -> m (Result, Solution)
-solveOptimized op goal mStep mDebug = refine Unknown mempty goal
+solveOptimized op goal mStep mDebug = refine Unsat mempty goal 0
   where
-    refine oldRes oldSol target = do
+    refine oldRes oldSol target n_pushes = do
       res <- checkSat
       case res of
         Sat   -> do
@@ -329,9 +329,16 @@ solveOptimized op goal mStep mDebug = refine Unknown mempty goal
               push
               let step = fromMaybe id mStep
               assert $ target `op` step (encode targetSol)
-              refine res sol target
-        _ -> do
-          pop
-          case mStep of
-            Nothing -> return (oldRes, oldSol)
-            Just _  -> solveOptimized op goal Nothing mDebug -- make sure the very last step did not skip the optimal result
+              refine res sol target (n_pushes + 1)
+        r -> do
+          if n_pushes < 1
+          then return (r, mempty)
+          else case mStep of
+            Nothing -> do
+              replicateM_ n_pushes pop
+              return (oldRes, oldSol)
+            Just _ -> do
+              pop
+              opt <- solveOptimized op goal Nothing mDebug -- make sure the very last step did not skip the optimal result
+              replicateM_ (n_pushes - 1) pop
+              return opt