From 1c11a82a7dc8b10a13b73cb6db20687f95ef627e Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 26 Sep 2022 20:57:55 -0400
Subject: [PATCH] test: update doc guide

---
 doc/guide.md | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/doc/guide.md b/doc/guide.md
index 0a521b67..8bacd25a 100644
--- a/doc/guide.md
+++ b/doc/guide.md
@@ -209,11 +209,11 @@ We start with `p = q`.
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (false := false)
+  (p := true)
   (q := true)
-  ((box (= Bool p q)) := true)
   (true := true)
-  (p := true))
+  (false := false)
+  ([[ (= p q) ]] := true))
 ```
 
 It is satisfiable, and we got a model where "p" and "q" are both false.
@@ -246,11 +246,11 @@ Note that this doesn't affect satisfiability without assumptions:
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (false := false)
+  (p := true)
   (q := true)
-  ((box (= Bool p q)) := true)
   (true := true)
-  (p := true))
+  (false := false)
+  ([[ (= p q) ]] := true))
 ```
 
 We can therefore add more formulas and see where it leads us.
@@ -264,13 +264,13 @@ We can therefore add more formulas and see where it leads us.
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (false := false)
+  (p := true)
   (q := true)
-  ((box (= Bool p q)) := true)
   (r := true)
-  ((box (or r (not p) false)) := true)
   (true := true)
-  (p := true))
+  (false := false)
+  ([[ (= p q) ]] := true)
+  ([[ (or r (not p) false) ]] := true))
 ```
 
 Still satisfiable, but now we see `r` in the model, too. And now:
@@ -331,12 +331,12 @@ We can play with assertions now:
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
  (model
-  (b := 0)
+  (true := true)
   (false := false)
-  ((box (<= (+ a ((* -1) b)) 0)) := true)
-  ($_le_comb[0] := 0)
   (a := 0)
-  (true := true))
+  (b := 0)
+  ([[ (<= (+ a ((* -1) b)) 0) ]] := true)
+  ($_le_comb[0] := 0))
 
 
 # let a_geq_1 = LRA_term.geq tstore a (LRA_term.const tstore (Q.of_int 1));;