diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,14 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v1.2.0 _(2024-07-11)_
+
+### Added
+- Added n-ary comparisons `distinct` & `equal`
+
+### Changed
+- *(breaking change)* When using `interactiveWith` the `SMTOption` `Incremental` is no longer set by default anymore
+
 ## v1.1.2 _(2024-07-02)_
 
 ### Changed
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.1.2
+version:               1.2.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
diff --git a/src/Language/Hasmtlib/Boolean.hs b/src/Language/Hasmtlib/Boolean.hs
--- a/src/Language/Hasmtlib/Boolean.hs
+++ b/src/Language/Hasmtlib/Boolean.hs
@@ -2,7 +2,7 @@
 
 module Language.Hasmtlib.Boolean where
 
-import Prelude (Bool(..), (.), id, Eq(..))  
+import Prelude (Bool(..), (.), id, Eq(..))
 import qualified Prelude as P
 import Data.Bit
 import Data.Coerce
@@ -10,7 +10,7 @@
 import Data.Foldable hiding (and, or)
 import qualified Data.Vector.Unboxed.Sized as V
 import GHC.TypeNats
-  
+
 class Boolean b where
   -- | Lift a 'Bool'
   bool :: Bool -> b
@@ -40,7 +40,7 @@
 
   -- | Exclusive-or
   xor :: b -> b -> b
- 
+
   infixr 3 &&
   infixr 2 ||
   infixr 0 ==>
@@ -81,11 +81,11 @@
   (||)  = (P.||)
   not   = P.not
   xor   = (/=)
-  
+
 instance Boolean Bit where
   bool = Bit
-  (&&) = (.&.) 
-  (||) = (.|.) 
+  (&&) = (.&.)
+  (||) = (.|.)
   not  = complement
   xor  = Bits.xor
 
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -1,10 +1,11 @@
 {-# LANGUAGE DefaultSignatures #-}
 -- required for DefaultEncoded a
-{-# LANGUAGE UndecidableInstances #-}  
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
 
 module Language.Hasmtlib.Codec where
 
-import Prelude hiding (not, (&&), (||))
+import Prelude hiding (not, (&&), (||), all, and)
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
@@ -12,11 +13,13 @@
 import Language.Hasmtlib.Boolean
 import Data.Kind
 import Data.Coerce
+import qualified Data.List as List
 import Data.Map (Map)
 import Data.Sequence (Seq)
-import Data.IntMap as IM
+import Data.IntMap as IM hiding (foldl)
 import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
+import qualified Data.Vector.Sized as V
 import Control.Monad
 
 -- | Compute the default 'Decoded' 'Type' for every functor-wrapper.
@@ -56,8 +59,15 @@
   decode sol (Div x y)          = liftA2 (/)   (decode sol x) (decode sol y)
   decode sol (LTH x y)          = liftA2 (<)   (decode sol x) (decode sol y)
   decode sol (LTHE x y)         = liftA2 (<=)  (decode sol x) (decode sol y)
-  decode sol (EQU x y)          = liftA2 (==)  (decode sol x) (decode sol y)
-  decode sol (Distinct x y)     = liftA2 (/=)  (decode sol x) (decode sol y)
+  decode sol (EQU xs)           = do
+    xs' <- decode sol (V.toList xs)
+    case xs' of
+      []   -> return true
+      (x:xs'') -> return $ all (x ==) xs''
+  decode sol (Distinct xs)      = do
+    xs' <- decode sol (V.toList xs)
+    let xss = List.filter ((==2) . length) $ List.permutations xs'
+    return $ all (\case (a:b:_) -> a /= b ; _ -> true) xss
   decode sol (GTHE x y)         = liftA2 (>=)  (decode sol x) (decode sol y)
   decode sol (GTH x y)          = liftA2 (>)   (decode sol x) (decode sol y)
   decode sol (Not x)            = fmap   not  (decode sol x)
@@ -77,7 +87,7 @@
   decode sol (ToReal x)         = fmap realToFrac (decode sol x)
   decode sol (ToInt x)          = fmap truncate   (decode sol x)
   decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)
-  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
+  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f)
   decode sol (BvNot x)          = fmap not (decode sol x)
   decode sol (BvAnd x y)        = liftA2 (&&) (decode sol x) (decode sol y)
   decode sol (BvOr x y)         = liftA2 (||) (decode sol x) (decode sol y)
@@ -103,7 +113,7 @@
   decode sol (ArrStore i x arr) = liftM3 arrStore (decode sol i) (decode sol x) (decode sol arr)
   decode _ (ForAll _ _)         = Nothing
   decode _ (Exists _ _)         = Nothing
-  
+
   encode = Constant . wrapValue
 
 instance Codec () where
diff --git a/src/Language/Hasmtlib/Equatable.hs b/src/Language/Hasmtlib/Equatable.hs
--- a/src/Language/Hasmtlib/Equatable.hs
+++ b/src/Language/Hasmtlib/Equatable.hs
@@ -7,20 +7,21 @@
 import Prelude hiding (not, (&&))
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Boolean
-import GHC.Generics
-import Numeric.Natural
 import Data.Int
 import Data.Word
 import Data.Void
+import qualified Data.Vector.Sized as V
+import Numeric.Natural
+import GHC.Generics
 
 -- | Test two as on equality as SMT-Expression.
--- 
+--
 -- @
 --     x <- var @RealType
---     y <- var 
+--     y <- var
 --     assert $ y === x && not (y /== x)
 -- @
--- 
+--
 class Equatable a where
   -- | Test whether two values are equal in the SMT-Problem.
   (===) :: a -> a -> Expr BoolSort
@@ -34,9 +35,9 @@
 infix 4 ===, /==
 
 instance (KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) where
-  (===) = EQU
-  {-# INLINE (===) #-}  
-  (/==) = Distinct
+  x === y = EQU $ V.fromTuple (x,y)
+  {-# INLINE (===) #-}
+  x /== y = Distinct $ V.fromTuple (x,y)
   {-# INLINE (/==) #-}
 
 class GEquatable f where
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -11,11 +11,14 @@
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Boolean
 import Data.GADT.Compare
-import Data.Map
+import Data.Map hiding (toList)
+import Data.List (intercalate)
 import Data.Kind
 import Data.Proxy
 import Data.Coerce
+import Data.Foldable (toList)
 import Data.ByteString.Builder
+import qualified Data.Vector.Sized as V
 import Control.Lens
 import GHC.TypeLits
 
@@ -126,11 +129,11 @@
 sortSing' _ = sortSing @t
 
 -- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k
--- 
+--
 -- @
 -- AllC '[]       k = ()
 -- AllC (c ': cs) k = (c k, AllC cs k)
--- @ 
+-- @
 type AllC :: [k -> Constraint] -> k -> Constraint
 type family AllC cs k :: Constraint where
   AllC '[]       k = ()
@@ -141,7 +144,7 @@
   SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
 
 -- | An existential wrapper that hides some known 'SMTSort'.
-type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f 
+type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
 
 -- | A SMT expression.
 --   For internal use only.
@@ -160,8 +163,8 @@
 
   LTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
   LTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  EQU       :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  Distinct  :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+  EQU       :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort
+  Distinct  :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort
   GTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
   GTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
 
@@ -227,7 +230,7 @@
   {-# INLINE not #-}
   xor  = Xor
   {-# INLINE xor #-}
-  
+
 instance KnownNat n => Boolean (Expr (BvSort n)) where
   bool = Constant . BvValue . bool
   {-# INLINE bool #-}
@@ -239,11 +242,11 @@
   {-# INLINE not #-}
   xor  = BvXor
   {-# INLINE xor #-}
-  
+
 instance Bounded (Expr BoolSort) where
   minBound = false
   maxBound = true
-  
+
 instance KnownNat n => Bounded (Expr (BvSort n)) where
   minBound = Constant $ BvValue minBound
   maxBound = Constant $ BvValue maxBound
@@ -289,8 +292,8 @@
 
   render (LTH x y)    = renderBinary "<" x y
   render (LTHE x y)   = renderBinary "<=" x y
-  render (EQU x y)    = renderBinary "=" x y
-  render (Distinct x y) = renderBinary "distinct" x y
+  render (EQU xs)     = renderNary "=" $ V.toList xs
+  render (Distinct xs)= renderNary "distinct" $ V.toList xs
   render (GTHE x y)   = renderBinary ">=" x y
   render (GTH x y)    = renderBinary ">" x y
 
@@ -373,8 +376,8 @@
   show (Div x y)            = "(" ++ show x ++ " / " ++ show y ++ ")"
   show (LTH x y)            = "(" ++ show x ++ " < " ++ show y ++ ")"
   show (LTHE x y)           = "(" ++ show x ++ " <= " ++ show y ++ ")"
-  show (EQU x y)            = "(" ++ show x ++ " == " ++ show y ++ ")"
-  show (Distinct x y)       = "(" ++ show x ++ " /= " ++ show y ++ ")"
+  show (EQU xs)             = "(= " ++ intercalate " " (show <$> toList xs) ++ ")"
+  show (Distinct xs)        = "(distinct " ++ intercalate " " (show <$> toList xs) ++ ")"
   show (GTHE x y)           = "(" ++ show x ++ " >= " ++ show y ++ ")"
   show (GTH x y)            = "(" ++ show x ++ " > " ++ show y ++ ")"
   show (Not x)              = "(not " ++ show x ++ ")"
diff --git a/src/Language/Hasmtlib/Internal/Expr/Num.hs b/src/Language/Hasmtlib/Internal/Expr/Num.hs
--- a/src/Language/Hasmtlib/Internal/Expr/Num.hs
+++ b/src/Language/Hasmtlib/Internal/Expr/Num.hs
@@ -5,10 +5,9 @@
 import Language.Hasmtlib.Integraled
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Equatable
-import Language.Hasmtlib.Orderable  
-import Data.Proxy
+import Language.Hasmtlib.Orderable
 import GHC.TypeNats
-  
+
 instance Num (Expr IntSort) where
    fromInteger = Constant . IntValue
    {-# INLINE fromInteger #-}
@@ -42,7 +41,7 @@
    {-# INLINE signum #-}
 
 instance KnownNat n => Num (Expr (BvSort n)) where
-   fromInteger = Constant . BvValue . fromInteger 
+   fromInteger = Constant . BvValue . fromInteger
    {-# INLINE fromInteger #-}
    (+)         = BvAdd
    {-# INLINE (+) #-}
@@ -54,7 +53,7 @@
    {-# INLINE abs #-}
    signum _    = 0
    {-# INLINE signum #-}
-   
+
 instance Fractional (Expr RealSort) where
   fromRational = Constant . RealValue . fromRational
   {-# INLINE fromRational #-}
@@ -90,15 +89,15 @@
 
 instance Integraled (Expr IntSort) where
   quot = IDiv
-  {-# INLINE quot #-}  
+  {-# INLINE quot #-}
   rem  = Mod
-  {-# INLINE rem #-}  
+  {-# INLINE rem #-}
   div  = IDiv
-  {-# INLINE div #-}  
+  {-# INLINE div #-}
   mod  = Mod
-  {-# INLINE mod #-}  
+  {-# INLINE mod #-}
   quotRem x y = (quot x y, rem x y)
-  {-# INLINE quotRem #-}  
+  {-# INLINE quotRem #-}
   divMod x y  = (div x y, mod x y)
   {-# INLINE divMod #-}
 
@@ -115,28 +114,3 @@
   {-# INLINE quotRem #-}
   divMod x y  = (div x y, mod x y)
   {-# INLINE divMod #-}
-
--- | Bitvector shift left
-bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-bvShL    = BvShL
-{-# INLINE bvShL #-}
-
--- | Bitvector logical shift right
-bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-bvLShR   = BvLShR
-{-# INLINE bvLShR #-}
-
--- | Concat two bitvectors
-bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
-bvConcat = BvConcat
-{-# INLINE bvConcat #-}
-
--- | Rotate bitvector left
-bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
-bvRotL   = BvRotL
-{-# INLINE bvRotL #-}
-
--- | Rotate bitvector right
-bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
-bvRotR   = BvRotR
-{-# INLINE bvRotR #-}
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -1,12 +1,13 @@
 module Language.Hasmtlib.Internal.Render where
 
 import Data.ByteString.Builder
+import Data.Foldable (foldl')
 import GHC.TypeNats
 
 -- | Render values to their SMTLib2-Lisp form, represented as @Builder@.
 class Render a where
   render :: a -> Builder
-   
+
 instance Render Bool where
   render b = if b then "true" else "false"
   {-# INLINEABLE render #-}
@@ -42,3 +43,9 @@
 renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
 renderTernary op x y z = "(" <> op <> " " <> render x <> " " <> render y <> " " <> render z <> ")"
 {-# INLINEABLE renderTernary #-}
+
+renderNary :: Render a => Builder -> [a] -> Builder
+renderNary op xs = "(" <> op <> renderedXs <> ")"
+  where
+    renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs
+{-# INLINEABLE renderNary #-}
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Language.Hasmtlib.Type.Expr
  ( SMTSort(..)
@@ -7,27 +8,50 @@
  , Value(..), unwrapValue, wrapValue
  , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort, AllC
  , Expr
+ , equal, distinct
+ , bvShL, bvLShR, bvConcat, bvRotL, bvRotR
  , for_all , exists
  , select, store
- , module Language.Hasmtlib.Internal.Expr.Num
  )
 where
 
 import Language.Hasmtlib.Internal.Expr
-import Language.Hasmtlib.Internal.Expr.Num
+import Language.Hasmtlib.Internal.Expr.Num ()
+import Language.Hasmtlib.Boolean
+import Data.Proxy
+import Data.List (genericLength)
+import Data.Foldable (toList)
+import qualified Data.Vector.Sized as V
+import GHC.TypeNats
 
+-- | Test multiple expressions on equality within in the 'SMT'-Problem.
+equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
+equal (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of
+  SomeNat n -> case V.fromListN' n xs of
+    Nothing  -> EQU $ V.fromTuple (a,b)
+    Just xs' -> EQU $ xs' V.++ V.fromTuple (a,b)
+equal (toList -> _)        = true
+
+-- | Test multiple expressions on distinctness within in the 'SMT'-Problem.
+distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
+distinct (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of
+  SomeNat n -> case V.fromListN' n xs of
+    Nothing  -> Distinct $ V.fromTuple (a,b)
+    Just xs' -> Distinct $ xs' V.++ V.fromTuple (a,b)
+distinct (toList -> _)        = true
+
 -- | A universal quantification for any specific 'SMTSort'.
 --   If the type cannot be inferred, apply a type-annotation.
 --   Nested quantifiers are also supported.
--- 
+--
 --   Usage:
 --
 --   @
 --   assert $
 --      for_all @IntSort $ \x ->
---         x + 0 === x && 0 + x === x 
---   @   
--- 
+--         x + 0 === x && 0 + x === x
+--   @
+--
 --   The lambdas 'x' is all-quantified here.
 --   It will only be scoped for the lambdas body.
 for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
@@ -36,16 +60,16 @@
 -- | An existential quantification for any specific 'SMTSort'
 --   If the type cannot be inferred, apply a type-annotation.
 --   Nested quantifiers are also supported.
--- 
+--
 --   Usage:
--- 
+--
 --   @
 --   assert $
 --      for_all @(BvSort 8) $ \x ->
 --          exists $ \y ->
---            x - y === 0 
---   @   
--- 
+--            x - y === 0
+--   @
+--
 --   The lambdas 'y' is existentially quantified here.
 --   It will only be scoped for the lambdas body.
 exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
@@ -58,3 +82,28 @@
 -- | Store a value in an array.
 store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
 store = ArrStore
+
+-- | Bitvector shift left
+bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+bvShL    = BvShL
+{-# INLINE bvShL #-}
+
+-- | Bitvector logical shift right
+bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+bvLShR   = BvLShR
+{-# INLINE bvLShR #-}
+
+-- | Concat two bitvectors
+bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
+bvConcat = BvConcat
+{-# INLINE bvConcat #-}
+
+-- | Rotate bitvector left
+bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
+bvRotL   = BvRotL
+{-# INLINE bvRotL #-}
+
+-- | Rotate bitvector right
+bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
+bvRotR   = BvRotR
+{-# INLINE bvRotR #-}
diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs
--- a/src/Language/Hasmtlib/Type/Solver.hs
+++ b/src/Language/Hasmtlib/Type/Solver.hs
@@ -1,9 +1,7 @@
 module Language.Hasmtlib.Type.Solver where
 
 import Language.Hasmtlib.Type.Pipe
-import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Solution
-import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Codec
 import qualified SMTLIB.Backends as B
 import qualified SMTLIB.Backends.Process as P
@@ -37,62 +35,62 @@
 -- main = do
 --   res <- solveWith (solver cvc5) $ do
 --     setLogic \"QF_LIA\"
--- 
+--
 --     x <- var @IntSort
--- 
+--
 --     assert $ x >? 0
---     
+--
 --     return x
--- 
+--
 --   print res
 -- @
 solveWith :: (Monad m, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
 solveWith solver m = do
   (a, problem) <- runStateT m def
   (result, solution) <- solver problem
-    
+
   return (result, decode solution a)
 
 -- | Pipes an SMT-problem interactively to the solver.
 --   Enables incremental solving by default.
 --   Here is a small example of how to use it for solving a problem utilizing the solvers incremental stack:
--- 
+--
 -- @
 -- import Language.Hasmtlib
 -- import Control.Monad.IO.Class
--- 
+--
 -- main :: IO ()
 -- main = do
 --   cvc5Living <- interactiveSolver cvc5
 --   interactiveWith cvc5Living $ do
+--     setOption $ Incremental True
 --     setOption $ ProduceModels True
 --     setLogic \"QF_LIA\"
--- 
+--
 --     x <- var @IntSort
--- 
+--
 --     assert $ x >? 0
--- 
+--
 --     (res, sol) <- solve
 --     liftIO $ print res
 --     liftIO $ print $ decode sol x
--- 
+--
 --     push
 --     y <- var @IntSort
--- 
+--
 --     assert $ y <? 0
 --     assert $ x === y
--- 
+--
 --     res' <- checkSat
 --     liftIO $ print res'
 --     pop
--- 
+--
 --     res'' <- checkSat
 --     liftIO $ print res''
--- 
+--
 --   return ()
 -- @
 interactiveWith :: (MonadIO m, WithSolver s) => (B.Solver, P.Handle) -> StateT s m () -> m ()
 interactiveWith (solver, handle) m = do
-   liftIO $ B.command_ solver $ render (Incremental True)
    _ <- runStateT m $ withSolver solver
    liftIO $ P.close handle