From 0f21cf069eb3293f687a62f82210681d5a8cb49b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 29 Aug 2022 20:28:42 -0400
Subject: [PATCH] test: update expected results

---
 Makefile                        |  3 +++
 doc/guide.md                    | 30 +++++++++++++++---------------
 unittest/core-logic/t1.expected | 14 +++++++-------
 3 files changed, 25 insertions(+), 22 deletions(-)

diff --git a/Makefile b/Makefile
index b6197567..3f30014d 100644
--- a/Makefile
+++ b/Makefile
@@ -27,6 +27,9 @@ clean:
 test:
 	@dune runtest $(OPTS) --force --no-buffer
 
+test-promote:
+	@dune runtest $(OPTS) --force --no-buffer --auto-promote
+
 TESTOPTS ?= -j $(J) -c tests/benchpress.sexp --progress
 TESTTOOL=benchpress
 DATE=$(shell date +%FT%H:%M)
diff --git a/doc/guide.md b/doc/guide.md
index 71c44f7e..52380000 100644
--- a/doc/guide.md
+++ b/doc/guide.md
@@ -209,10 +209,10 @@ We start with `p = q`.
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (false := $@c[0])
   (q := true)
-  ((= Bool p q) := true)
   (true := true)
+  ((= Bool p q) := true)
+  (false := $@c[0])
   (p := true))
 ```
 
@@ -246,10 +246,10 @@ Note that this doesn't affect satisfiability without assumptions:
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (false := $@c[0])
   (q := false)
-  ((= Bool p q) := true)
   (true := true)
+  ((= Bool p q) := true)
+  (false := $@c[0])
   (p := false))
 ```
 
@@ -264,12 +264,12 @@ We can therefore add more formulas and see where it leads us.
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (false := $@c[0])
   (q := false)
   (r := true)
+  (true := true)
   ((= Bool p q) := true)
   ((or r (not p) false) := true)
-  (true := true)
+  (false := $@c[0])
   (p := false))
 ```
 
@@ -331,20 +331,20 @@ We can play with assertions now:
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
+  (+ := $@c[4])
   (a := 0)
-  ((+ a) := $@c[0])
+  ((+ a) := $@c[2])
   (0 := 0)
-  (false := $@c[5])
   (b := 0)
-  ((+ a ((* -1) b)) := $@c[7])
-  ((<= (+ a ((* -1) b))) := $@c[3])
-  ((* -1) := $@c[6])
+  ((+ a ((* -1) b)) := $@c[0])
+  ((<= (+ a ((* -1) b))) := $@c[6])
+  ((* -1) := $@c[5])
+  (true := true)
   ((<= (+ a ((* -1) b)) 0) := true)
   (((* -1) b) := $@c[1])
-  (<= := $@c[2])
-  ($_le_comb[0] := 0)
-  (+ := $@c[4])
-  (true := true))
+  (<= := $@c[3])
+  (false := $@c[7])
+  ($_le_comb[0] := 0))
 
 
 # let a_geq_1 = LRA_term.geq tstore a (LRA_term.const tstore (Q.of_int 1));;
diff --git a/unittest/core-logic/t1.expected b/unittest/core-logic/t1.expected
index 42a1949f..37c23abb 100644
--- a/unittest/core-logic/t1.expected
+++ b/unittest/core-logic/t1.expected
@@ -4,21 +4,21 @@ type tower: [Type;Type(1);Type(2);Type(3);Type(4)]
 Bool: [true, false]
 a: a, b: b, typeof(a): Bool
 b2b: (Bool -> Bool)
-p(a): p a
-p(b): p b
-q(a): q a
-q(b): q b
+p(a): (p a)
+p(b): (p b)
+q(a): (q a)
+q(b): (q b)
 typeof(p a): Bool
-lxy_px: (\x:Bool. (\y:Bool. p x[1]))
+lxy_px: (\x:Bool. (\y:Bool. (p x[1])))
   type: (Bool -> (Bool -> Bool))
   type of type: Type
-lxy_px a b: ((\x:Bool. (\y:Bool. p x[1]))) a b
+lxy_px a b: ((\x:Bool. (\y:Bool. (p x[1]))) a b)
   type: Bool
 (=): =
   type: (Pi A:Type. (Pi _:A[0]. (A[1] -> Bool)))
 p2: p2
   type: (tau -> (tau -> Bool))
-t2: = ((tau -> (tau -> Bool))) ((\x:tau. (\y:tau. p2 x[1] y[0]))) (= tau)
+t2: (= (tau -> (tau -> Bool)) (\x:tau. (\y:tau. (p2 x[1] y[0]))) (= tau))
   type: Bool
 f_vec: vec
   type: (Type -> (nat -> Type))