2 ms·
I'm suspicious of the theorem proving example. I thought Z3 could fail to return sat or unsat, but he is assuming that if it's not sat the theorem must be prov
by jeremysalwen 7mo ago
I'm suspicious of the theorem proving example. I thought Z3 could fail to return sat or unsat, but he is assuming that if it's not sat the theorem must be proven
- hwayne 7mo ago...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.
- ymherklotz 7mo agoNo I think it's fine. On another note, I have proven Fermat's Last Theorem with z3 using this setup :) and it goes faster if you reduce a variable called "timeout" for some reason! from z3 import * s = Solver() s.set("timeout", 600) a = Int('a') b = Int('b') c = Int('c') s.add(a > 0) s.add(b > 0) s.add(c > 0) theorem = a ** 3 + b ** 3 != c ** 3 if s.check(Not(theorem)) == sat: print(f"Counterexample: {s.model()}") else: print("Theorem true")