Counter Example found for Arithmetic Laws

[leuschel]

The tool says the checked in example ArithmeticLaws.mch is not correct (after the initialisation x=-3, y=-3, z=-3).

[wysiib]

I fixed a part of the problem by simplifying the translation of BOOL and INTEGER. However, the issue of the solver returning UNKNOWN remains.

[x-moe-x]

It might be a good Idea to enable ModelCheckingResult to reflect check-sat = unknown

[x-moe-x]

testIssue59JustInvariant() leads to following solver stack (which produces check-sat = unknown):

(declare-fun x () Int)
(assert
    (let
        ((a!1
            (exists ((x Int))
                (let
                    ((a!1
                        ((as union (Array Int Bool))
                              (store ((as const (Array Int Bool)) false) x true)
                              (store (store ((as const (Array Int Bool)) false) 1 true) 2 true)
                        )
                    ))
                    (= a!1 (store (store ((as const (Array Int Bool)) false) 1 true) 2 true)
                    )
                )
            )
        ))
        (and (= (^ x 2) (* x x)) a!1)
    )
)
(check-sat)

[x-moe-x]

simplified version still produces check-sat = unknown in z3:

; prepare set = {1,2}
(declare-const set (Array Int Bool))
(assert (= set (store (store ((as const (Array Int Bool)) false) 1 true) 2 true)))
; prepare x
(declare-fun x () Int)
(assert (= (^ x 2) (* x x)))
; assert existence of y with y U set = set
(assert
  (exists ((y Int))
    (let
      ((setUnion
          ((as union (Array Int Bool))
                (store ((as const (Array Int Bool)) false) y true)
                set
          )
      ))
      (= setUnion set
      )
    )
  )
)
(check-sat)

[x-moe-x]

if we remove the line (assert (= (^ x 2) (* x x))) it's satisfiable again...

[wysiib]

maybe exponentiation is the weakness here? we could think about rewriting to multiplication if the exponent in a constant. What's the result if we add (assert (= (* x x) (* x x))) instead of (assert (= (^ x 2) (* x x)))?

[x-moe-x]

Strangely the following code produces also check-sat = unknown

(declare-fun x () Int)
(assert (= (^ x 2) (* x x)))
(check-sat)

[wysiib]

Apparently, support for non-linear integer arithmetic is not great in Z3: http://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic/13898524#13898524

I really think we should investigate whether we could set up a special case for translation of exponentiation if the exponent is a constant. So far, I do not see another option (aside of using several backends). However, I am not sure how translation / rewrite rules should be applied on top of our parser. Maybe there is a better way than to introduce a special case in the translation. Maybe @dohan has an idea?

[x-moe-x]

Is using (check-sat-using qfnra-nlsat) an option?

[x-moe-x]

Doesn't solve our problem anyways... It just solves

(declare-const x Int)
(assert (= (^ x 2) 16))
(check-sat-using qfnra-nlsat)

[x-moe-x]

We can not fix this issue now as z3 seems to be unable to recognize satisfiability for the combination of (^ x y) and the quantifier formula. Will open new issue for backlog...

[x-moe-x]

development continues in #67