I want to use Z3 to proof validity of statements like this:
∀ a b: ℤ, ~ b = 0 -> (a / b) ^ 2. = (a * a) / (b * b)
Or in SMT-LIB format:
(declare-fun b () Int)
(declare-fun a () Int)
(assert (=> (= b 0) false))
(assert (let ((a!1 (= (^ (/ (to_real a) (to_real b)) 2.0)
(/ (to_real (* a a)) (to_real (* b b))))))
(not a!1)))
(check-sat)
But I get timeout with the default tactic. I guess Z3 is wasting its time trying to instantiate numbers in order to find a solution. But I'm only interested in unsat output since the problem is generalized and a sat output doesn't mean anything. What combination of tactics I should use to find validity of simple algebraic statements like this?
When I run your script, I get unsat pretty quickly:
$ time z3 a.smt2
unsat
z3 a.smt2 0.17s user 0.01s system 97% cpu 0.191 total
Perhaps your z3 is too old? Here's the version I have:
$ z3 --version
Z3 version 4.12.0 - 64 bit
Try upgrading, I think the latest released version is 4.12.1.
If the issue persists and you have the latest z3, you should report this as a regression at https://github.com/Z3Prover/z3/issues