diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
index 4aaf2cf97..39dbdc4af 100644
--- a/copilot-theorem/CHANGELOG
+++ b/copilot-theorem/CHANGELOG
@@ -1,3 +1,6 @@
+2026-03-31
+        * Fix examples so they compile with latest copilot-theorem. (#692)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-theorem/examples/BoyerMoore.hs b/copilot-theorem/examples/BoyerMoore.hs
index d4cebf638..572673b10 100644
--- a/copilot-theorem/examples/BoyerMoore.hs
+++ b/copilot-theorem/examples/BoyerMoore.hs
@@ -5,7 +5,7 @@ module BoyerMoore where
 
 import Copilot.Language hiding (length)
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (induction, def, debug, z3)
 
 import Copilot.Core.Type
 
@@ -71,7 +71,7 @@ spec = do
     maj = majorityVote ss
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = False }
+induct = induction def { debug = False } z3
 
 -- | Initial value for a given type.
 --
diff --git a/copilot-theorem/examples/Grey.hs b/copilot-theorem/examples/Grey.hs
index 9a1ca4319..6a87864d8 100644
--- a/copilot-theorem/examples/Grey.hs
+++ b/copilot-theorem/examples/Grey.hs
@@ -4,7 +4,7 @@ module Grey where
 
 import Copilot.Language
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (def, Options (..), z3, kInduction, induction)
 
 import Prelude ()
 import Data.String (fromString)
@@ -32,7 +32,7 @@ spec = do
     r  = extern "reset" Nothing
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = False }
+induct = induction def { debug = False } z3
 
 kinduct :: Word32 -> Proof Universal
-kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False }
+kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3
diff --git a/copilot-theorem/examples/Incr.hs b/copilot-theorem/examples/Incr.hs
index 3c39a008d..cb028df6e 100644
--- a/copilot-theorem/examples/Incr.hs
+++ b/copilot-theorem/examples/Incr.hs
@@ -4,7 +4,7 @@ import Prelude ()
 import Copilot.Language
 
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (def, induction, debug, z3)
 
 spec = do
   bounds <- prop "bounds" (forAll $ x < 255)
@@ -16,4 +16,4 @@ spec = do
     x = [2] ++ (1 + x)
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = True }
+induct = induction def { debug = True } z3
diff --git a/copilot-theorem/examples/SerialBoyerMoore.hs b/copilot-theorem/examples/SerialBoyerMoore.hs
index 5f0d42092..8b4ebdf9e 100644
--- a/copilot-theorem/examples/SerialBoyerMoore.hs
+++ b/copilot-theorem/examples/SerialBoyerMoore.hs
@@ -4,7 +4,7 @@ module SerialBoyerMoore where
 
 import Copilot.Language
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (def, Options (..), induction, kInduction, z3)
 
 import Prelude ()
 import Data.String (fromString)
@@ -56,7 +56,7 @@ spec = do
     (p, s, j) = majority input
 
 induct :: Proof Universal
-induct = induction def { nraNLSat = False, debug = False }
+induct = induction def { debug = False } z3
 
 kinduct :: Word32 -> Proof Universal
-kinduct k = kInduction def { nraNLSat = False, startK = k, maxK = k, debug = False }
+kinduct k = kInduction def { startK = k, maxK = k, debug = False } z3
diff --git a/copilot-theorem/examples/SphericalWCV.hs b/copilot-theorem/examples/SphericalWCV.hs
index 74b899583..e1d128a30 100644
--- a/copilot-theorem/examples/SphericalWCV.hs
+++ b/copilot-theorem/examples/SphericalWCV.hs
@@ -8,7 +8,7 @@ import Prelude ()
 import Copilot.Language
 import Copilot.Language.Reify
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (def, debug, onlySat, onlyValidity, z3)
 
 import qualified Copilot.Language.Operators.Propositional as P
 
@@ -241,7 +241,7 @@ localConvexity = do
   theorem "6"  (P.not (forAll $ locallyConvex tau)) arithSat
 
 arith :: Proof Universal
-arith    = onlyValidity def { nraNLSat = True, debug = False }
+arith    = onlyValidity def { debug = False } z3
 
 arithSat :: Proof Existential
-arithSat = onlySat      def { nraNLSat = True, debug = False }
+arithSat = onlySat      def { debug = False } z3
diff --git a/copilot-theorem/examples/WCV.hs b/copilot-theorem/examples/WCV.hs
index 62c27f287..8aa7f8b5e 100644
--- a/copilot-theorem/examples/WCV.hs
+++ b/copilot-theorem/examples/WCV.hs
@@ -5,7 +5,7 @@ import Prelude ()
 import Copilot.Language
 import Copilot.Language.Reify
 import Copilot.Theorem
-import Copilot.Theorem.Prover.Z3
+import Copilot.Theorem.Prover.SMT (def, debug, onlySat, onlyValidity, z3)
 
 import qualified Copilot.Language.Operators.Propositional as P
 
@@ -165,7 +165,7 @@ localConvexity = do
   theorem "6"  (P.not (forAll $ locallyConvex tau)) arithSat
 
 arith :: Proof Universal
-arith    = onlyValidity def { nraNLSat = True, debug = False }
+arith    = onlyValidity def { debug = False } z3
 
 arithSat :: Proof Existential
-arithSat = onlySat      def { nraNLSat = True, debug = False }
+arithSat = onlySat      def { debug = False } z3