diff --git a/docs/tactics/linarith.md b/docs/tactics/linarith.md
index c8af995..e4627ac 100644
--- a/docs/tactics/linarith.md
+++ b/docs/tactics/linarith.md
@@ -91,7 +91,7 @@ Similar to `Linarith()`, but now applies to order of magnitude inequalities rath
 Example:
 ```
 >>> from estimates.main import *
->>> p = loglinarith_imposssible_example()
+>>> p = loglinarith_impossible_example()
 Starting proof.  Current proof state:
 N: pos_int
 x: pos_real
diff --git a/src/estimates/linprog.py b/src/estimates/linprog.py
index 636a47c..c557274 100644
--- a/src/estimates/linprog.py
+++ b/src/estimates/linprog.py
@@ -4,7 +4,7 @@
 
 from sympy import Pow
 
-from z3 import Real, Solver, Sum, sat, simplify
+from z3 import Real, Solver, Sum, is_true, sat, simplify
 
 # exact linear programming tools.
 
@@ -173,9 +173,16 @@ def feasibility(inequalities: list[Inequality]) -> tuple[bool, dict]:
             f"Farkas lemma violation!  Problem is neither feasible nor infeasible. Inequalities: {inequalities}"
         )
 
-def is_valid_counterexample(dict):
-    for var, value in dict.items():
-        if isinstance(var, Pow) and var.base in dict:
-            if simplify(dict[var.base] ** var.exp) != value:
+def is_valid_counterexample(assignment: dict) -> bool:
+    """Check that powered variables match their bases in a Z3 model assignment.
+
+    Z3's ``!=`` / ``==`` return BoolRef objects; using them in a Python ``if``
+    raises ``Z3Exception: Symbolic expressions cannot be cast to concrete
+    Boolean values``. Use ``is_true`` for a concrete check instead.
+    """
+    for var, value in assignment.items():
+        if isinstance(var, Pow) and var.base in assignment:
+            computed = simplify(assignment[var.base] ** var.exp)
+            if not is_true(simplify(computed == value)):
                 return False
     return True
diff --git a/src/estimates/main.py b/src/estimates/main.py
index 9a19258..11edb0e 100644
--- a/src/estimates/main.py
+++ b/src/estimates/main.py
@@ -236,7 +236,7 @@ def loglinarith_hard_solution2() -> None:
     p.use(LogLinarith())
 
 
-def loglinarith_imposssible_example() -> ProofAssistant:
+def loglinarith_impossible_example() -> ProofAssistant:
     p = ProofAssistant()
     N = p.var("pos_int", "N")
     x, y = p.vars("pos_real", "x", "y")
@@ -246,8 +246,12 @@ def loglinarith_imposssible_example() -> ProofAssistant:
     return p
 
 
+# Keep the old misspelling as an alias for existing docs/call sites.
+loglinarith_imposssible_example = loglinarith_impossible_example
+
+
 def loglinarith_failure_example() -> None:
-    p = loglinarith_imposssible_example()
+    p = loglinarith_impossible_example()
     p.use(LogLinarith(verbose=True))