-
When given the following benchmark: (benchmark example :status sat :logic QF_LIA :extrafuns ((a Int) (b Int)) :formula (not (implies (= a b) (= (* a a) (* b b)))) ;:formula (not (implies (and (= a 0) (= 0 b)) ; (= (* a a) (* b b))) ) Z3 responds with partitions: *2 {a b} -> 0:int sat yet when the...
-
First, I should say,Z3 is a exciting tools! When I use Z3, Z3_pop's the second param description is confusing, I don't know how to set this param. Is num_scopes equal to the number of Z3_assert_cnstr I have called after Z3_push? or something else? I use Z3_pop like this : .....Add some constraints...
-
Hello - I apologize up-front for the newbie question. I'm trying to get started using the Z3 C API, and am looking for documentation for getting the environment situated, building, linking, and executing programs which use this API. I'm on a windows machine and have LCC, but also Cygwin with...
-
Is it possible to deal with tuples in Z3 with the Simplify format? I've tried what I would consider the more likely possibilities for functions, i.e. mk_tuple, tuple, etc., but nothing so far.