Test failures on newer z3 versions

[numinit]

Hi there,

I get the following failures when using the latest z3/haskell-z3 versions:

haskell-z3: this commit: b77a17e
z3: Z3 version 4.12.6 - 64 bit (note that I am able to reproduce this on the latest 4.13.4 as well, but not on 4.11.x)
Linux: Linux monomyth 6.12.5-xanmod1 #1-NixOS SMP PREEMPT_DYNAMIC Tue Jan 1 00:00:00 UTC 1980 x86_64 GNU/Linux

Failures:

  test/Z3/Base/Spec.hs:544:11: 
  1) Z3.Base.Tactics mkTactic, applyTactic, repeatTactic, applyResultToString
       expected: (goals
                 (goal
                   (or (not (<= (- 2.0) y)) (not (<= y (- 2.0))))
                   (not (<= 0.0 y)))
                 )
        but got: (goals
                 (goal
                   (or (not (<= 0.0 x)) (not (<= x 0.0)))
                   (not (<= 2.0 x)))
                 )

  To rerun use: --match "/Z3.Base/Tactics/mkTactic, applyTactic, repeatTactic, applyResultToString/" --seed 1407078955

  test/Z3/Tutorial.hs:21:42: 
  2) Z3.Tutorial, Section: Strategies, Section: Introduction, Apply simplify and solve-eq tactics
       expected: (goals
                 (goal
                   (not (<= y (- 2.0)))
                   (not (<= y 0.0)))
                 )
        but got: (goals
                 (goal
                   (not (<= x 0.0))
                   (not (<= x 2.0)))
                 )

  To rerun use: --match "/Z3.Tutorial/Section: Strategies/Section: Introduction/Apply simplify and solve-eq tactics/" --seed 1407078955

Randomized with seed 1407078955

[arminhoh]

Hi,

I can confirm your failing tests for this commit and I think the tests should be adapted, as this just seems to be a change in the tactics of z3. Specifically a different variable is eliminated first, when applying solve-eq. Both simplification examples still produce an equivalent goal.

To verify the first example, I encoded it in smtlib and got the same result, as in the test case.

(declare-const x Real)
(declare-const y Real)

(assert (or (< x 0.0) (> x 0.0)))
(assert (= x (+ y 2.0)))
(assert (< y 0.0))

(apply (then simplify solve-eqs))

gives me

(goals
(goal
  (or (not (<= 0.0 x)) (not (<= x 0.0)))
  (not (<= 2.0 x))
  :precision precise :depth 2)
)

As the second example is from the tutorial, I checked the output there and also matches the test result.

I adapted the tests and cabal test runs through now. I prepared a pull request for the changes. #95

Cheers

[numinit]

Awesome, thank you!