-
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...
-
I am trying to use the mod (Integer modulus) operator in my formula. Even though I saw that mod is acceptable operator, in the output it comes out as an uninterpreted function. Could someone point to a small toy example for mod and div operators? Thanks. rajesh