diff --git a/cabal.project.dist b/cabal.project.dist
index 6912f53b..56534353 100644
--- a/cabal.project.dist
+++ b/cabal.project.dist
@@ -2,7 +2,6 @@ packages: .
           submodules/llvm-pretty
           submodules/parameterized-utils
           submodules/what4/what4
-          submodules/what4-serialize
           submodules/crucible/crucible
           submodules/crucible/crucible-symio
           submodules/crucible/crucible-llvm
diff --git a/pate.cabal b/pate.cabal
index a0cbf47b..0ef2dcd8 100644
--- a/pate.cabal
+++ b/pate.cabal
@@ -40,8 +40,9 @@ common shared
                        elf-edit >= 0.39,
                        IntervalMap >= 0.6 && < 0.7,
                        lens >= 4 && < 6,
-                       hashtables >= 1.2 && < 1.3,
-                       mtl >= 2 && < 2.3,
+                       hashtables >= 1.2 && < 1.3.1,
+                       mtl >= 2 && < 2.4,
+                       monadplus,
                        panic >= 0.4 && < 0.5,
                        lumberjack >= 0.1 && < 1.1,
                        prettyprinter >= 1.7 && < 1.8,
@@ -55,7 +56,6 @@ common shared
                        split >= 0.2,
                        parameterized-utils,
                        what4 >= 1 && < 2,
-                       what4-serialize,
                        crucible,
                        crucible-llvm,
                        macaw-base,
@@ -68,7 +68,7 @@ common shared
                        demangler >= 1.3.0.0,
                        semmc,
                        sayable,
-                       text >= 1 && < 1.3,
+                       text >= 1 && < 2.1,
                        tomland >= 1.3 && < 1.4,
                        transformers,
                        time >= 1 && < 2,
@@ -198,6 +198,25 @@ common shared-test
                  text,
                  pate 
 
+-- just used for loading test modules interactively
+library pate-test-base
+  import: shared-test
+  hs-source-dirs: tests, arch
+  other-modules: Pate.AArch32, Pate.PPC
+  build-depends: semmc-aarch32,
+                 macaw-aarch32,
+                 macaw-aarch32-symbolic,
+                 macaw-loader-aarch32,
+                 macaw-ppc,
+                 macaw-ppc-symbolic,
+                 macaw-loader-ppc,
+                 semmc-ppc,
+                 asl-translator,
+                 what4,
+                 dismantle-arm-xml,
+                 dismantle-ppc,
+                 dismantle-tablegen
+
 test-suite pate-test-loaders
   import: shared-test
   type: exitcode-stdio-1.0
@@ -250,6 +269,20 @@ test-suite pate-test-aarch32
                  what4,
                  dismantle-arm-xml
 
+test-suite pate-test-solver
+  import: shared-test
+  type: exitcode-stdio-1.0
+  main-is: SolverTestMain.hs
+  other-modules: Pate.AArch32
+  hs-source-dirs: tests, arch
+  build-depends: semmc-aarch32,
+                 macaw-aarch32,
+                 macaw-aarch32-symbolic,
+                 macaw-loader-aarch32,
+                 asl-translator,
+                 what4,
+                 dismantle-arm-xml
+
 common shared-exec
   ghc-options: -Wall -Wcompat
   default-language: Haskell2010
diff --git a/submodules/asl-translator b/submodules/asl-translator
index e5633daa..dacd5220 160000
--- a/submodules/asl-translator
+++ b/submodules/asl-translator
@@ -1 +1 @@
-Subproject commit e5633daaea5a709bedc9216bfe799c3be798fafa
+Subproject commit dacd522014ca172e4d78ae6b65f41cedd027d1c8
diff --git a/submodules/crucible b/submodules/crucible
index 1d2d95d2..3af4ac55 160000
--- a/submodules/crucible
+++ b/submodules/crucible
@@ -1 +1 @@
-Subproject commit 1d2d95d232eb2aae076d68021e1d75d322968595
+Subproject commit 3af4ac55ccc4ae4b30388d068936fc9a2fbfb85d
diff --git a/submodules/dismantle b/submodules/dismantle
index 48433e7c..1599d970 160000
--- a/submodules/dismantle
+++ b/submodules/dismantle
@@ -1 +1 @@
-Subproject commit 48433e7ccb02924b2f4695c8c9f09fb9cfccdfc4
+Subproject commit 1599d9707498bff1fee9ed1a37804675c79eee08
diff --git a/submodules/flexdis86 b/submodules/flexdis86
index c19b55e3..5370202a 160000
--- a/submodules/flexdis86
+++ b/submodules/flexdis86
@@ -1 +1 @@
-Subproject commit c19b55e3bfe3147484c8b26bb12b56b29678d4b1
+Subproject commit 5370202ab9563cb9a0a15475aa801e9b37fa5ab4
diff --git a/submodules/llvm-pretty b/submodules/llvm-pretty
index 64d43d93..94e38484 160000
--- a/submodules/llvm-pretty
+++ b/submodules/llvm-pretty
@@ -1 +1 @@
-Subproject commit 64d43d9375a819dc2a2df99fb98df24f049dcfaa
+Subproject commit 94e384842b214ba72446d1694446fb5261ab6ce2
diff --git a/submodules/macaw b/submodules/macaw
index 7d93e7a5..ddea3058 160000
--- a/submodules/macaw
+++ b/submodules/macaw
@@ -1 +1 @@
-Subproject commit 7d93e7a546c709240d2ab3ebce24dd4fefff8ab7
+Subproject commit ddea30584337973186c3eedefb27414eedad60a5
diff --git a/submodules/macaw-loader b/submodules/macaw-loader
index 7e26fbe5..342b6eb7 160000
--- a/submodules/macaw-loader
+++ b/submodules/macaw-loader
@@ -1 +1 @@
-Subproject commit 7e26fbe5b68edbfe40adc4c9285401da12bf0a88
+Subproject commit 342b6eb7f2344d98732b897877e1699dc0a8551e
diff --git a/submodules/parameterized-utils b/submodules/parameterized-utils
index a888f586..95869cd6 160000
--- a/submodules/parameterized-utils
+++ b/submodules/parameterized-utils
@@ -1 +1 @@
-Subproject commit a888f5862b73a1575d36fef9327fcbe3dbcbff51
+Subproject commit 95869cd611c037aea6446599fdba9c0984b8635c
diff --git a/submodules/semmc b/submodules/semmc
index a3b8b89b..2147ee3e 160000
--- a/submodules/semmc
+++ b/submodules/semmc
@@ -1 +1 @@
-Subproject commit a3b8b89b9e88c94aab2ec6e06f993edcc9126cea
+Subproject commit 2147ee3e7b966ca635289efa742f9e5f4c7bb540
diff --git a/submodules/what4 b/submodules/what4
index 835238d8..076f49b9 160000
--- a/submodules/what4
+++ b/submodules/what4
@@ -1 +1 @@
-Subproject commit 835238d87500d48c3b0ae9121f2b484b71faa8b5
+Subproject commit 076f49b996bd328764a9c6edece6b7c34cb1cfb4
diff --git a/tools/pate-repl/Repl.hs b/tools/pate-repl/Repl.hs
index 2ac954fe..b21db1c0 100644
--- a/tools/pate-repl/Repl.hs
+++ b/tools/pate-repl/Repl.hs
@@ -32,7 +32,8 @@ import qualified System.IO as IO
 import qualified System.IO.Unsafe as IO
 import qualified Data.IORef as IO
 import qualified Control.Concurrent as IO
-import           Control.Monad.State ( MonadState, StateT, modify, gets, runStateT, get, put, forM )
+import           Control.Monad ( forM )
+import           Control.Monad.State ( MonadState, StateT, modify, gets, runStateT, get, put )
 import qualified Control.Monad.IO.Class as IO
 import           Data.Proxy
 import qualified Data.Text.IO as Text