adapt tests for simplify/solve-eqs tactic

This change fixes IagoAbal#94. Both the tutorial examples and another example, failed due to change in z3's simplify/solve-eq tactics. The tests are adapted accordingly.

Author: arminhoh

test/Z3/Base/Spec.hs

@@ -541,5 +541,5 @@ spec = around withContext $ do
           simplify <- Z3.mkTactic ctx "solve-eqs"
           tactic <- Z3.repeatTactic ctx simplify 10
           Z3.applyResultToString ctx =<< Z3.applyTactic ctx tactic goal)
-          `shouldReturn` "(goals\n(goal\n  (or (not (<= (- 2.0) y)) (not (<= y (- 2.0))))\n  (not (<= 0.0 y)))\n)"
+          `shouldReturn` "(goals\n(goal\n  (or (not (<= 0.0 x)) (not (<= x 0.0)))\n  (not (<= 2.0 x)))\n)"
 

test/Z3/Tutorial.hs

@@ -18,7 +18,7 @@ spec = do
   describe "Section: Strategies" $ do
     describe "Section: Introduction" $ do
       it "Apply simplify and solve-eq tactics" $
-        Z3.Monad.evalZ3 simplifySolveEqs `shouldReturn` "(goals\n(goal\n  (not (<= y (- 2.0)))\n  (not (<= y 0.0)))\n)"
+        Z3.Monad.evalZ3 simplifySolveEqs `shouldReturn` "(goals\n(goal\n  (not (<= x 0.0))\n  (not (<= x 2.0)))\n)"
       it "Apply split-clause tactic" $
         Z3.Monad.evalZ3 applySplitClause `shouldReturn` "(goals\n(goal\n  (< x 0.0)\n  (= x (+ y 1.0))\n  (< y 0.0))\n(goal\n  (> x 0.0)\n  (= x (+ y 1.0))\n  (< y 0.0))\n)"