fix: Z3 counterexample check and impossible_example spelling

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

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

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))