diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,8 +1,19 @@
 # HasCacBDD Changelog
 
-## upcoming
+## v0.4.0.0 (2026-06-20)
 
-- ...
+- rewrite "Show" and "Read" instances using "top", "bot", "var", "ifthenelse" and parsec for "Read". This should make them lawful.
+
+## v0.3.0.1 (2025-10-22)
+
+- let `svgGraph` try to find the `dot` executable in multiple common locations. This should make it work on non-Linux systems. (Thanks to @MitchBoontjes for the original patch.)
+- add tests for `Data.HasCacBDD.Visuals` module.
+
+## v0.3.0.0 (2025-01-01)
+
+- add `optimalOrder`
+- fix segfault on Apple M1 and ARM aarch64
+- minor improvements of documentation and tests
 
 ## v0.2.0.0 (2023-11-23)
 
diff --git a/HasCacBDD.cabal b/HasCacBDD.cabal
--- a/HasCacBDD.cabal
+++ b/HasCacBDD.cabal
@@ -1,5 +1,5 @@
 name:                HasCacBDD
-version:             0.2.0.0
+version:             0.4.0.0
 synopsis:            Haskell bindings for CacBDD
 homepage:            https://github.com/m4lvin/HasCacBDD
 license:             GPL-2
@@ -30,19 +30,21 @@
 
 source-repository head
   type:     git
-  location: git://github.com/m4lvin/HasCacBDD.git
+  location: https://github.com/m4lvin/HasCacBDD.git
 
 custom-setup
   setup-depends:       base >= 4.8 && < 5,
-                       Cabal < 3.9,
-                       directory
+                       Cabal < 3.13,
+                       directory <1.4
 
 library
   exposed-modules:     Data.HasCacBDD,
                        Data.HasCacBDD.Visuals
   build-depends:       base >=4.8 && < 5,
+                       parsec >= 3.1 && < 3.2,
                        process >= 1.1 && < 1.7,
-                       QuickCheck >= 2.4 && < 2.15
+                       QuickCheck >= 2.4 && < 2.15,
+                       directory < 1.4
   default-language:    Haskell2010
   hs-source-dirs:      hs
   extra-libraries:     stdc++, CacBDD
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -3,8 +3,8 @@
 
 [![Release](https://img.shields.io/github/release/m4lvin/HasCacBDD.svg)](https://github.com/m4lvin/HasCacBDD/releases)
 [![Hackage](https://img.shields.io/hackage/v/HasCacBDD.svg)](https://hackage.haskell.org/package/HasCacBDD)
-[![GitLab CI](https://gitlab.com/m4lvin/HasCacBDD/badges/master/pipeline.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)
-[![Test Coverage](https://gitlab.com/m4lvin/HasCacBDD/badges/master/coverage.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/master/file/hpc/combined/all/hpc_index.html?job=test)
+[![GitLab CI](https://gitlab.com/m4lvin/HasCacBDD/badges/main/pipeline.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/pipelines)
+[![Test Coverage](https://gitlab.com/m4lvin/HasCacBDD/badges/main/coverage.svg)](https://gitlab.com/m4lvin/HasCacBDD/-/jobs/artifacts/main/file/hpc/combined/all/hpc_index.html?job=test)
 
 Haskell bindings for CacBDD, a Binary Decision Diagram (BDD) package with dynamic cache management.
 
@@ -33,10 +33,14 @@
 
 3. Now you can play with Boolean functions :-)
 
-       λ> import Data.HasCacBDD
-       λ> var 5
-       Var 5 Top Bot
-       λ> neg (var 5)
-       Var 5 Bot Top
-       λ> dis (neg (var 3)) (var 3)
-       Top
+       ghci> import Data.HasCacBDD
+       ghci> var 5
+       var 5
+       ghci> neg (var 5)
+       neg (var 5)
+       ghci> dis (neg (var 3)) (var 3)
+       top
+       ghci> dis (neg (var 1)) (var 3)
+       ifthenelse (var 1) (var 3) top
+
+For further documentation, see <https://hackage.haskell.org/package/HasCacBDD/docs/Data-HasCacBDD.html>
diff --git a/c/BDDNodeC.cpp b/c/BDDNodeC.cpp
--- a/c/BDDNodeC.cpp
+++ b/c/BDDNodeC.cpp
@@ -7,21 +7,21 @@
 
 int BDD_Variable(BDD* this_ptr) { return this_ptr->Variable(); }
 
-BDD BDD_Then(const BDD* this_ptr) { return this_ptr->Then(); }
+void BDD_Then(BDD* ret_ptr, const BDD* this_ptr) { *ret_ptr = this_ptr->Then(); }
 
-BDD BDD_Else(const BDD* this_ptr) { return this_ptr->Else(); }
+void BDD_Else(BDD* ret_ptr, const BDD* this_ptr) { *ret_ptr = this_ptr->Else(); }
 
-BDD BDD_Exist(BDD* this_ptr, const BDD* cube) { return this_ptr->Exist(*cube); }
+void BDD_Exist(BDD* ret_ptr, BDD* this_ptr, const BDD* cube) { *ret_ptr = this_ptr->Exist(*cube); }
 
-BDD BDD_Universal(BDD* this_ptr, const BDD* cube) { return this_ptr->Universal(*cube); }
+void BDD_Universal(BDD* ret_ptr, BDD* this_ptr, const BDD* cube) { *ret_ptr = this_ptr->Universal(*cube); }
 
-BDD BDD_Restrict(const BDD* this_ptr, const BDD* other) { return this_ptr->Restrict(*other); }
+void BDD_Restrict(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = this_ptr->Restrict(*other); }
 
-BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other) { return this_ptr->Compose(v, *other); }
+void BDD_Compose(BDD* ret_ptr, const BDD* this_ptr, int v, const BDD* other) { *ret_ptr = this_ptr->Compose(v, *other); }
 
-BDD BDD_Permute(const BDD* this_ptr, const vector<int>* permu) { return this_ptr->Permute(*permu); }
+void BDD_Permute(BDD* ret_ptr, const BDD* this_ptr, const vector<int>* permu) { *ret_ptr = this_ptr->Permute(*permu); }
 
-BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube) { return this_ptr->AndExist(*other, *cube); }
+void BDD_AndExist(BDD* ret_ptr, BDD* this_ptr, const BDD* other, const BDD* cube) { *ret_ptr = this_ptr->AndExist(*other, *cube); }
 
 bool BDD_IsComp(BDD* this_ptr) { bool b = this_ptr->IsComp(); return b; }
 
@@ -29,32 +29,32 @@
 
 XBDDManager* XBDDManager_new(int varCount) { return new XBDDManager(varCount); }
 
-BDD XBDDManager_BddOne(XBDDManager* this_ptr) { return (BDD) this_ptr->BddOne(); }
+void XBDDManager_BddOne(BDD* ret_ptr, XBDDManager* this_ptr) { *ret_ptr = this_ptr->BddOne(); }
 
-BDD XBDDManager_BddZero(XBDDManager* this_ptr) { return (BDD) this_ptr->BddZero(); }
+void XBDDManager_BddZero(BDD* ret_ptr, XBDDManager* this_ptr) { *ret_ptr = this_ptr->BddZero(); }
 
-BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex) { BDD bar = this_ptr->BddVar(varIndex); return bar; }
+void XBDDManager_BddVar(BDD* ret_ptr, XBDDManager* this_ptr, int varIndex) { *ret_ptr = this_ptr->BddVar(varIndex); }
 
-BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { return (BDD) this_ptr->Ite(*f, *g, *h); }
+void XBDDManager_Ite(BDD* ret_ptr, XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h) { *ret_ptr = this_ptr->Ite(*f, *g, *h); }
 
 const XManager* XBDDManager_manager(const XBDDManager* this_ptr) { return this_ptr->manager(); }
 
-BDD BDD_Operator_Not(const BDD* this_ptr) { BDD bar = (! *this_ptr); return bar;  }
+void BDD_Operator_Not(BDD* ret_ptr, const BDD *this_ptr) { *ret_ptr = (!*this_ptr); }
 
 bool BDD_Operator_Equal(const BDD* this_ptr, const BDD* other) { bool b = (*this_ptr == *other); return b; }
 
-BDD BDD_Operator_Or(const BDD* this_ptr, const BDD* other) { BDD bar = (*this_ptr + *other); return bar; }
+void BDD_Operator_Or(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr + *other); }
 
-BDD BDD_Operator_And(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr * *other); }
+void BDD_Operator_And(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr * *other); }
 
-BDD BDD_Operator_Xor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr ^ *other); }
+void BDD_Operator_Xor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr ^ *other); }
 
-BDD BDD_Operator_LessEqual(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr <= *other); }
+void BDD_Operator_LessEqual(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr <= *other); }
 
-BDD BDD_Operator_Nor(const BDD* this_ptr, const BDD* other) { return (BDD) (*this_ptr % *other); }
+void BDD_Operator_Nor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr % *other); }
 
-BDD BDD_Operator_Nand(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr | *other); }
+void BDD_Operator_Nand(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr | *other); }
 
-BDD BDD_Operator_XNor(const BDD* this_ptr, const BDD* other) { return(BDD) (*this_ptr & *other); }
+void BDD_Operator_XNor(BDD* ret_ptr, const BDD* this_ptr, const BDD* other) { *ret_ptr = (*this_ptr & *other); }
 
-void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime) { return this_ptr->ShowInfo(); }
+void XBDDManager_ShowInfo(XBDDManager* this_ptr) { this_ptr->ShowInfo(); }
diff --git a/c/BDDNodeC.h b/c/BDDNodeC.h
--- a/c/BDDNodeC.h
+++ b/c/BDDNodeC.h
@@ -5,35 +5,37 @@
 BDD* BDD_new();
 const XManager* BDD_checkSameManager(const BDD* this_ptr, const BDD* other);
 int BDD_Variable(BDD* this_ptr);
-BDD BDD_Then(const BDD* this_ptr);
-BDD BDD_Else(const BDD* this_ptr);
-BDD BDD_Exist(BDD* this_ptr, const BDD* cube);
-BDD BDD_Universal(BDD* this_ptr, const BDD* cube);
-BDD BDD_Restrict(const BDD* this_ptr, const BDD* other);
-BDD BDD_Compose(const BDD* this_ptr, int v, const BDD* other);
-BDD BDD_Permute(const BDD* this_ptr, const vector<int>* permu);
-BDD BDD_AndExist(BDD* this_ptr, const BDD* other, const BDD* cube);
+void BDD_Then(BDD* ret_ptr, const BDD* this_ptr);
+void BDD_Else(BDD* ret_ptr, const BDD* this_ptr);
+void BDD_Exist(BDD* ret_ptr, BDD* this_ptr, const BDD* cube);
+void BDD_Universal(BDD* ret_ptr, BDD* this_ptr, const BDD* cube);
+void BDD_Restrict(BDD* ret_ptr, const BDD* this_ptr, const BDD* other);
+void BDD_Compose(BDD* ret_ptr, const BDD* this_ptr, int v, const BDD* other);
+void BDD_Permute(BDD* ret_ptr, const BDD* this_ptr, const vector<int>* permu);
+void BDD_AndExist(BDD* ret_ptr, BDD* this_ptr, const BDD* other, const BDD* cube);
 bool BDD_IsComp(BDD* this_ptr);
 const XManager* BDD_manager(const BDD* this_ptr);
 
 // In C we can not overload operators, so we use functions instead.
-BDD BDD_Operator_Not       (const BDD* this_ptr); // !
+void BDD_Operator_Not       (BDD* ret_ptr, const BDD* this_ptr); // !
+
 bool BDD_Operator_Equal    (const BDD* this_ptr, const BDD* other); // ==
-BDD BDD_Operator_Or        (const BDD* this_ptr, const BDD* other); // +
-BDD BDD_Operator_And       (const BDD* this_ptr, const BDD* other); // *
-BDD BDD_Operator_Xor       (const BDD* this_ptr, const BDD* other); // ^
-BDD BDD_Operator_LessEqual (const BDD* this_ptr, const BDD* other); // <=
-BDD BDD_Operator_Nor       (const BDD* this_ptr, const BDD* other); // %
-BDD BDD_Operator_Nand      (const BDD* this_ptr, const BDD* other); // |
-BDD BDD_Operator_XNor      (const BDD* this_ptr, const BDD* other); // &
+void BDD_Operator_Or        (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // +
+void BDD_Operator_And       (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // *
+void BDD_Operator_Xor       (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // ^
+void BDD_Operator_LessEqual (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // <=
+void BDD_Operator_Nor       (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // %
+void BDD_Operator_Nand      (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // |
+void BDD_Operator_XNor      (BDD* ret_ptr, const BDD* this_ptr, const BDD* other); // &
 
+
 XBDDManager* XBDDManager_new(int varCount);
-BDD XBDDManager_BddOne(XBDDManager* this_ptr);
-BDD XBDDManager_BddZero(XBDDManager* this_ptr);
-BDD XBDDManager_BddVar(XBDDManager* this_ptr, int varIndex);
-BDD XBDDManager_Ite(XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h);
+void XBDDManager_BddOne(BDD* ret_ptr, XBDDManager* this_ptr);
+void XBDDManager_BddZero(BDD* ret_ptr, XBDDManager* this_ptr);
+void XBDDManager_BddVar(BDD* ret_ptr, XBDDManager* this_ptr, int varIndex);
+void XBDDManager_Ite(BDD* ret_ptr, XBDDManager* this_ptr, const BDD* f, const BDD* g, const BDD* h);
 
-void XBDDManager_ShowInfo(XBDDManager* this_ptr, double vtime);
+void XBDDManager_ShowInfo(XBDDManager* this_ptr);
 
 const XManager* XBDDManager_manager(const XBDDManager* this_ptr);
 }
diff --git a/hs/Data/HasCacBDD.hs b/hs/Data/HasCacBDD.hs
--- a/hs/Data/HasCacBDD.hs
+++ b/hs/Data/HasCacBDD.hs
@@ -20,20 +20,23 @@
   firstVarOf, maxVarOf, allVarsOf, allVarsOfSorted,
   -- * Sub-BDDs and length
   thenOf, elseOf, subsOf, sizeOf,
+  -- * Variable Orderings
+  optimalOrder,
   -- * Show and convert to trees
   BddTree(..), unravel, ravel,
   -- * Print some debugging information
   maximumvar, showInfo
 ) where
 
-import Control.Arrow (Arrow(first))
 import Foreign.C (CInt(..))
 import Foreign.Ptr (Ptr)
 import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)
 import System.IO.Unsafe (unsafePerformIO)
-import Data.List (nub,(\\),sort)
-import Data.Maybe (fromJust)
+import Data.Function (on)
+import Data.List ((\\), minimumBy, nub, permutations, sort)
+import Data.Maybe (fromJust, listToMaybe)
 import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf)
+import Text.Parsec
 
 -- | The CacBDD datatype has no structure because
 -- from our perspective BDDs are just pointers.
@@ -52,16 +55,16 @@
 type CacXBddManager = ()
 newtype XBddManager = XBddManager (ForeignPtr CacXBddManager)
 
-type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO (Ptr CacBDD)
-type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)
-type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)
+type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO ()
+type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO ()
+type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO ()
 
-foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: Word -> IO (Ptr CacBDD)
+foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: IO (Ptr CacBDD)
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_new" xBddManager_new :: CInt -> IO (Ptr CacXBddManager)
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_ShowInfo" xBddManager_showInfo :: Ptr CacXBddManager -> IO ()
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddOne"  xBddManager_BddOne  :: NullOp
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddZero" xBddManager_BddZero :: NullOp
-foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar"  xBddManager_BddVar  :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO (Ptr CacBDD)
+foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar"  xBddManager_BddVar  :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO ()
 foreign import ccall unsafe "BDDNodeC.h XBDDManager_Ite"     xBddManager_Ite     :: Ptr CacBDD -> Ptr CacXBddManager -> BinaryOp
 foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Equal"  bdd_Operator_Equal  :: Ptr CacBDD -> Ptr CacBDD -> IO Bool
 foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Not"    bdd_Operator_Not    :: UnaryOp
@@ -85,19 +88,25 @@
 
 fromManager :: NullOp -> Bdd
 fromManager nulloperator = let (XBddManager mptr) = manager in
-  finalize $ unsafePerformIO $
-    withForeignPtr mptr $ nulloperator (unsafePerformIO (bdd_new 8))
+  finalize $ unsafePerformIO $ do
+    b <- bdd_new
+    withForeignPtr mptr $ nulloperator b
+    return b
 {-# NOINLINE fromManager #-}
 
 withBDD :: UnaryOp -> Bdd -> Bdd
-withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $
-  withForeignPtr fptr $ unioperator (unsafePerformIO (bdd_new 8))
+withBDD unioperator (Bdd fptr) = finalize $ unsafePerformIO $ do
+  b <- bdd_new
+  withForeignPtr fptr $ unioperator b
+  return b
 {-# NOINLINE withBDD #-}
 
 withTwoBDDs :: BinaryOp -> Bdd -> Bdd -> Bdd
-withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $
+withTwoBDDs binoperator (Bdd fptr1) (Bdd fptr2) = finalize $ unsafePerformIO $ do
+  b <- bdd_new
   withForeignPtr fptr1 $
-    withForeignPtr fptr2 . binoperator (unsafePerformIO (bdd_new 8))
+    withForeignPtr fptr2 . binoperator b
+  return b
 {-# NOINLINE withTwoBDDs #-}
 
 fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a
@@ -165,11 +174,13 @@
 ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
 ifthenelse (Bdd test) (Bdd yes) (Bdd no) =
   let (XBddManager mptr) = manager in
-    finalize $ unsafePerformIO $
+    finalize $ unsafePerformIO $ do
+      b <- bdd_new
       withForeignPtr test (\t ->
         withForeignPtr yes (\y ->
           withForeignPtr no (\n ->
-            withForeignPtr mptr (\m -> xBddManager_Ite (unsafePerformIO (bdd_new 8)) m t y n))))
+            withForeignPtr mptr (\m -> xBddManager_Ite b m t y n))))
+      return b
 {-# NOINLINE ifthenelse #-}
 
 instance Eq Bdd where
@@ -268,7 +279,7 @@
       m1 = maxVarOf $ thenOf b
       m2 = maxVarOf $ elseOf b
 
--- | All variables in a given BDD, *not* sorted, lazy.
+-- | All variables in a given BDD, /not/ sorted, lazy.
 allVarsOf :: Bdd -> [Int]
 allVarsOf b
   | b == bot = []
@@ -282,7 +293,7 @@
 allVarsOfSorted = sort . allVarsOf
 
 -- | List all node / sub-BDDs of a given BDD.
--- This includes the root node of b itself, but omits terminal nodes.
+-- This includes the root node, but omits terminal nodes.
 subsOf :: Bdd -> [Bdd]
 subsOf = subsOf' [] where
   subsOf' done b
@@ -297,12 +308,29 @@
 sizeOf = length . subsOf
 
 instance Show Bdd where
-  show = show . unravel
+  showsPrec d b = f (d > 10) (unravel b) where
+    f :: Bool -> BddTree -> ShowS
+    f _ Bot = ("bot" ++)
+    f _ Top = ("top" ++)
+    f p (Var n Top Bot) = showParen p (("var " ++ show n) ++)
+    f p (Var n Bot Top) = showParen p (("neg (var " ++ show n ++ ")") ++)
+    f p (Var n a c) = showParen p
+      (("ifthenelse (var " ++ show n ++ ") " ++ f True a "" ++ " " ++ f True c "") ++)
 
 instance Read Bdd where
-  readsPrec k input = map (first ravel) (readsPrec k input)
+  readsPrec _ input = either (const []) return (parse pBdd "" input)
 
--- | A simple tree definition to show BDDs as text.
+-- | Parser for 'Bdd' values, used by the 'Read' instance.
+pBdd :: Parsec String () (Bdd,String)
+pBdd = (,) <$> pExp <*> getInput where -- No "<* eof" here, but getInput for readList.
+  pExp = spaces >> (pAtom <|> pIfThenElse <|> pNeg)
+  pAtom = (pConst <|> pVar <|> (char '(' *> pExp <* char ')')) <* spaces
+  pConst = (string "top" >> return top) <|> (string "bot" >> return bot)
+  pVar =  string "var " >> (var . read <$> many1 digit)
+  pNeg = string "neg " >> neg <$> pAtom
+  pIfThenElse = string "ifthenelse " >> spaces >> ifthenelse <$> pAtom <*> pAtom <*> pAtom
+
+-- | A tree definition that is also used to 'show' values ot the 'Bdd' type.
 data BddTree = Bot | Top | Var Int BddTree BddTree deriving (Eq,Read,Show)
 
 -- | Convert a BDD to a tree.
@@ -358,20 +386,20 @@
 -- | Given a set of all variables, complete an assignment.
 completeAss :: [Int] -> Assignment -> [Assignment]
 completeAss allvars ass =
-  if null (addvars ass)
-    then [ass]
-    else concatMap (completeAss allvars) (extend ass (head (addvars ass)))
+  case addvars ass of
+    [] -> [ass]
+    n:_ -> concatMap (completeAss allvars) (extend ass n)
   where
     addvars s = allvars \\ sort (map fst s)
     extend s v = [ (v,False):s, (v,True):s ]
 
--- | Get all complete assignments, given a set of all variables.
+-- | Get all complete assignments, given a list of variables.
 -- In particular this will include variables not in the BDD.
 allSatsWith :: [Int] -> Bdd -> [Assignment]
 allSatsWith allvars b = concatMap (completeAss allvars) (allSats b)
 
--- | Given a set of all variables, get the number of satisfying assignments.
--- Note that allvars must be nub'd and sorted.
+-- | Get the number of satisfying assignments, given a list of variables.
+-- Note that the given list must be nub'd and sorted.
 satCountWith :: [Int] -> Bdd -> Int
 satCountWith allvars b
   | b == top = 2 ^ length allvars
@@ -387,7 +415,7 @@
 anySatWith :: [Int] -> Bdd -> Maybe Assignment
 anySatWith allvars b = case anySat b of
   Nothing -> Nothing
-  Just partass -> Just $ head $ completeAss allvars partass
+  Just partass -> listToMaybe $ completeAss allvars partass
 
 -- | Relabel variables according to the given mapping.
 -- Note that the mapping list must be sorted!
@@ -427,6 +455,12 @@
     Just k  -> case lookup k repls of
       Nothing  -> ifthenelse (var k) (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)
       Just psi -> ifthenelse psi     (substitSimul repls $ thenOf b) (substitSimul repls $ elseOf b)
+
+-- | Find an optimal variable-reording.
+-- Returns a relabelling @r@ such that @sizeOf (relabel r b)@ is minimal.
+optimalOrder :: Bdd -> [(Int,Int)]
+optimalOrder b = minimumBy (compare `on` (\r -> sizeOf (relabel r b))) allPermut where
+  allPermut = map (zip (allVarsOf b)) $ permutations (allVarsOf b)
 
 -- | Show internal statistics.
 showInfo :: IO ()
diff --git a/hs/Data/HasCacBDD/Visuals.hs b/hs/Data/HasCacBDD/Visuals.hs
--- a/hs/Data/HasCacBDD/Visuals.hs
+++ b/hs/Data/HasCacBDD/Visuals.hs
@@ -1,13 +1,16 @@
--- | Very simple visualisation of BDDs using /dot/.
+-- | Visualisation of BDDs using the @dot@ program from [GraphViz](https://graphviz.org/).
 
 module Data.HasCacBDD.Visuals (
   genGraph,
   genGraphWith,
   showGraph,
-  svgGraph
+  svgGraph,
+  svgGraphWithPath,
 ) where
 
+import Control.Monad (filterM)
 import Data.Maybe (fromJust)
+import System.Directory (doesFileExist)
 import System.Exit
 import System.IO
 import System.Process
@@ -51,7 +54,8 @@
       rankings = concat [ "{ rank=same; "++ unwords (nodesOf v) ++ " }\n" | v <- allVarsOf myb ]
       nodesOf v = map (("n"++).show.snd) $ filter ( \(b,_) -> firstVarOf b == Just v ) topdone
 
--- | Display the graph of a BDD with dot.
+-- | Display the graph of a BDD with @\/usr\/bin\/dot -Tx11@.
+-- Only works on Linux. On other systems consider using 'svgGraph'.
 showGraph :: Bdd -> IO ()
 showGraph b = do
   (inp,_,_,pid) <- runInteractiveProcess "/usr/bin/dot" ["-Tx11"] Nothing Nothing
@@ -61,10 +65,32 @@
   _ <- waitForProcess pid
   return ()
 
--- | Generate SVG of a BDD with dot.
-svgGraph :: Bdd -> IO String
-svgGraph b = do
-  (exitCode,out,err) <- readProcessWithExitCode "/usr/bin/dot" ["-Tsvg" ] (genGraph b)
+-- | Generate SVG of a BDD with the @dot@ executable installed at the given path.
+svgGraphWithPath :: String -> Bdd -> IO String
+svgGraphWithPath dot b = do
+  (exitCode,out,err) <- readProcessWithExitCode dot ["-Tsvg" ] (genGraph b)
   case exitCode of
-    ExitSuccess -> return $ (unlines.tail.lines) out
+    ExitSuccess -> case lines out of
+      [] -> error "dot -Tsvg succeeded but did not provide any output."
+      _:rest -> return (unlines rest)
+      -- NOTE: we remove the first line of the output which is
+      -- "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
     ExitFailure n -> error $ "dot -Tsvg failed with exit code " ++ show n ++ " and error: " ++ err
+
+-- | Generate SVG of a BDD, trying default locations to find @dot@.
+svgGraph :: Bdd -> IO String
+svgGraph b = findDotPath >>= \ dot -> svgGraphWithPath dot b
+
+-- | Try to find the @dot@ executable at some default locations.
+-- Results in an error when the exectuable is not found.
+findDotPath :: IO FilePath
+findDotPath =
+  let dotPaths = [ "/usr/bin/dot"
+                 , "/opt/homebrew/bin/dot"
+                 , "C:\\Program Files\\Graphviz\\bin\\dot.exe"
+                 , "C:\\Program Files (x86)\\Graphviz\\bin\\dot.exe" ]
+  in do
+    results <- filterM doesFileExist dotPaths
+    case results of
+      dot:_ -> return dot
+      [] -> error "Cound not find 'dot' at a standard path. Please use svgGraphWithPath instead."
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,3 +1,3 @@
-resolver: lts-21.19
+resolver: lts-23.27
 packages:
 - '.'
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -1,22 +1,26 @@
-module Main where
+{-# OPTIONS_GHC -Wno-x-partial #-}
 
-import Data.HasCacBDD
-import Data.List (nub)
+module Main (main) where
+
+import Data.List ((\\),nub)
 import Data.Maybe (fromJust,isNothing)
 import Data.Tuple (swap)
 import Test.QuickCheck
 import Test.Hspec
 import Test.Hspec.QuickCheck
 
+import Data.HasCacBDD
+import Data.HasCacBDD.Visuals
+
 main :: IO ()
 main  = hspec $ do
   describe "Examples" $ do
-    describe "Creating BDDs" $ do
-      it "top == Top" $ show top `shouldBe` "Top"
-      it "show bot" $ show bot `shouldBe` "Bot"
-      it "show (var 1)" $ show (var 1) `shouldBe` "Var 1 Top Bot"
-      it "show (var 2)" $ show (var 1) `shouldBe` "Var 1 Top Bot"
-      it "show (var 3)" $ show (var 2) `shouldBe` "Var 2 Top Bot"
+    describe "Creating and showing BDDs" $ do
+      it "top == Top" $ show top `shouldBe` "top"
+      it "show bot" $ show bot `shouldBe` "bot"
+      it "show (var 1)" $ show (var 1) `shouldBe` "var 1"
+      it "show (var 2)" $ show (var 1) `shouldBe` "var 1"
+      it "show (var 3)" $ show (var 2) `shouldBe` "var 2"
     describe "Some tautologies" $ do
       it "bot == bot" $ bot `shouldBe` bot
       it "top == top" $ top `shouldBe` top
@@ -63,12 +67,11 @@
     it "imp (conSet [var 1,var 0]) (var 1) == top" $ imp (conSet [var 1,var 0]) (var 1) `shouldBe` top
     it "imp (conSet [var 0,var 1]) (var 0) == top" $ imp (conSet [var 0,var 1]) (var 0) `shouldBe` top
     it "imp (con (var 0) (var 1)) (var 0) == top" $ imp (con (var 0) (var 1)) (var 0) `shouldBe` top
-    it "show top == \"Top\"" $ show top `shouldBe` "Top"
-    it "show bot == \"Bot\"" $ show bot `shouldBe` "Bot"
+    it "show top == \"top\"" $ show top `shouldBe` "top"
+    it "show bot == \"bot\"" $ show bot `shouldBe` "bot"
   describe "QuickCheck Properties" $ do
     prop "selfEqual"      (\b -> (b::Bdd) == b)
     prop "showReadEqual"  (\b -> read (show b) == (b::Bdd))
-    prop "showReadTreeEq" (\b -> (ravel . read . show . unravel $ b) == b)
     prop "idSymmetry"     (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a))
     prop "singleNegation" (\b -> neg b /= b)
     prop "doubleNegation" (\b -> neg (neg b) == b)
@@ -86,7 +89,6 @@
     prop "allSats"        (\b -> all (\s -> restrictSet b s == top) (allSats b))
     prop "anySat"         (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top)
     prop "ifthenelse"     (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c))))
-    prop "ravel-unravel"  (\b -> b == ravel (unravel b))
     prop "firstVarOf"     (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b)
     prop "maxVarOf"       (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf   b)
     prop "thenOf"         (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True ))
@@ -116,16 +118,60 @@
                                       gnippam = map swap mapping
                                    in
                                       relabel gnippam (relabel mapping b) == b)
-    prop "relabelFun"    (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) == a)
-    prop "substit"       (\b c -> substit 5 b c == ifthenelse b (restrict c (5,True)) (restrict c (5,False)))
-    prop "show"          (\a b -> (show a == show b) == (a == (b::Bdd)))
-    prop "read"          (\b -> read (show b) == (b :: Bdd))
-    prop "showList"      (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))
-    prop "readList"      (\a b -> readList (show [a,b]) == [([unravel a, unravel b] :: [BddTree], "")])
+    prop "relabelFun"    (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) === a)
+    prop "substit"       (\b c -> substit 5 b c === ifthenelse b (restrict c (5,True)) (restrict c (5,False)))
+    prop "substit2"      (\b c -> substit (head ([0..] \\ allVarsOf c)) b c === c)
+    prop "substitSimul"  (\b -> substitSimul [] b === b)
+    prop "substitSimul2" (\b n -> substitSimul [(n,var n)] b === b)
+    prop "optimalOrder"  (\b -> sizeOf b < 15 ==> sizeOf (relabel (optimalOrder b) b) <= sizeOf b)
+  describe "Unraveling to BddTree" $ do
+    prop "ravel-unravel"  (\b -> b == ravel (unravel b))
+    prop "ravel-unravelN" (\b -> b /= ravel (unravel (neg b)))
+    prop "showReadTreeEq" (\b -> (ravel . read . show . unravel $ b) == b)
+    prop "treeShowReadEq" (\b -> (read . show . unravel $ b) == unravel b)
+    prop "treeEqIffEq"    (\a b -> (unravel a == unravel b) === (a == b))
+    prop "treeNEqIffEq"   (\a b -> (unravel a /= unravel b) === (a /= b))
+    prop "listShowRead"   (\a b c -> (read . show . map unravel $ [a,b,c]) == map unravel [a, b, c])
   describe "QuickCheck Expected Failures" $ do
+    prop "evaluate may return Nothing" $
+      expectFailure (\b ass -> evaluate b ass =/= Nothing)
     prop "wrong deMorganOne" $
       expectFailure (\a b -> neg (a `con` b) === (neg a `con` neg b))
     prop "wrong deMorganTwo" $
       expectFailure (\a b -> neg (a `dis` b) === (neg a `dis` neg b))
     modifyMaxSuccess (* 1000) $ prop "folding substit is not the same as substitSimul" $
       expectFailure (\b1 b2 c -> foldl (flip $ uncurry substit) c [(1,b1),(2,b2)] === substitSimul [(1,b1),(2,b2)] c)
+  describe "Visualisation" $ do
+    describe "genGraph" $ do
+      it "var 12345" $ genGraph (var 12345) `shouldContain` "12345"
+      it "top has no circles" $ genGraph top `shouldNotContain` "circle"
+      it "bot had no circles" $ genGraph bot `shouldNotContain` "circle"
+      it "bot /= top" $ genGraph bot /= genGraph top
+    describe "svgGraph" $ do
+      it "svgGraph top returns an svg" $
+        (svgGraph top >>= \ s -> return (take 13 s  == "<!DOCTYPE svg")) `shouldReturn` True
+      it "svgGraph top is short" $
+        (svgGraph top >>= \ s -> return (length s < 1000)) `shouldReturn` True
+      it "svgGraph (var 1) is longer" $
+        (svgGraph (var 1) >>= \ s -> return (length s > 1000)) `shouldReturn` True
+  describe "instances Show Bdd and Read Bdd" $ do
+    describe "show" $ do
+      it "var 1 `con` var 2" $ show (var 1 `con` var 2) `shouldBe` "ifthenelse (var 1) (var 2) bot"
+      prop "show ==" (\a b -> (show a == show b) === (a == (b::Bdd)))
+      prop "read ==" (\b -> read (show b) === (b :: Bdd))
+    describe "Pair for precendence test" $ do
+      it "show (P (var 3) top)" $ show (P (var 3) top) `shouldBe` "P (var 3) top"
+      it "show (P (var 3) (var 1 `con` var 2))" $ show (P (var 3) (var 1 `con` var 2)) `shouldBe` "P (var 3) (ifthenelse (var 1) (var 2) bot)"
+    describe "showList" $ do
+      prop "showList [a]"  (\a b -> (showList [a] "" == showList [b] "") === (a == (b::Bdd)))
+      prop "readList [a,b]" (\a b -> readList (show [a,b]) === [([a, b] :: [Bdd], "")])
+      prop "readList [...]" (\l -> readList (show l) === [(l :: [Bdd], "")])
+  describe "instance Read Bdd" $ do
+    describe "single BDD value" $ do
+      it "read \"var 1\"" $ read "var 1" `shouldBe` var 1
+      it "read \"ifthenelse (var 1) (var 2) (var 2)\"" $ read "ifthenelse (var 1) (var 2) (var 2)" `shouldBe` ifthenelse (var 1) (var 2) (var 2)
+    describe "list of BDDs" $ do
+      it "read \"[var 1, var 3]\"" $ read "[var 1, var 3]" `shouldBe` [var 1, var 3]
+      it "read \"[ top , ifthenelse ( var 3 ) bot bot]\"" $ read "[ top , ifthenelse ( var 3 ) bot bot]" `shouldBe` [top, bot]
+
+data Pair = P Bdd Bdd deriving (Show)