diff --git a/dependencies/what4 b/dependencies/what4
index 7b9f456..6f5e0fe 160000
--- a/dependencies/what4
+++ b/dependencies/what4
@@ -1 +1 @@
-Subproject commit 7b9f4563de467c9fdfe1f26f4f0fbd1f2c03d829
+Subproject commit 6f5e0fe9bef58234603ccf6914c32ea1ba2f9766
diff --git a/language-sally.cabal b/language-sally.cabal
index e5767b3..f534b28 100644
--- a/language-sally.cabal
+++ b/language-sally.cabal
@@ -27,7 +27,7 @@ common dependencies
   build-depends:
     , base                     >=4.8   && <4.16
     , parameterized-utils      >=2.0   && <2.2
-    , what4                    >=1.2
+    , what4                    >=1.3
     , what4-transition-system  >=0.0.3
 
 library
diff --git a/src/Language/Sally/Writer.hs b/src/Language/Sally/Writer.hs
index 1be12cf..4d799ad 100644
--- a/src/Language/Sally/Writer.hs
+++ b/src/Language/Sally/Writer.hs
@@ -230,6 +230,8 @@ instance SMTLib2Tweaks a => SMTWriter (SallyWriter a) where
 
   pushCommand _ = pure $ SMT2.push 1
   popCommand _ = pure $ SMT2.pop 1
+  push2Command _ = pure $ SMT2.push 2
+  pop2Command _ = pure $ SMT2.pop 2
   resetCommand _ = pure SMT2.resetAssertions
 
   checkCommands _ = [pure SMT2.checkSat]
@@ -238,6 +240,9 @@ instance SMTLib2Tweaks a => SMTWriter (SallyWriter a) where
 
   getUnsatAssumptionsCommand _ = pure SMT2.getUnsatAssumptions
   getUnsatCoreCommand _ = pure SMT2.getUnsatCore
+  getAbductCommand _ nm e = SMT2.getAbduct nm <$> e
+  getAbductNextCommand _ = pure SMT2.getAbductNext
+
   setOptCommand _ = (pure <$>) <$> SMT2.setOption
 
   declareCommand _proxy v argTypes retType =