From 4cb027c45fdd874baa89112576915f85ea5ee2e9 Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sun, 29 Oct 2017 22:05:26 +0100
Subject: [PATCH] update z3 part of the documentation as discussed in the
 meeting

---
 README.md | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 8b272d9..23d7a06 100644
--- a/README.md
+++ b/README.md
@@ -90,13 +90,10 @@ Currently there is only one frontend for the Java EDSL, but this could quite eas
 
 One of the implemented backends is for the [Z3 Theorem Prover](https://github.com/Z3Prover/z3). The `LogicIR.Expr` is converted to a `Z3 AST`.
 
-TODO: valid (invalid), satisfiable (unsatisfiable)
-TODO: 
+To determine if the expression `P == Q` is valid, we ask Z3 to prove that `P != Q` is unsatisfiable. There are three possible results:
 
-To determine if two expressions (`P` and `Q`) are equal, we ask Z3 to prove `P != Q`. There are three possible results:
-
-1. `Sat` -> Z3 proved `P != Q` is satisfiable, which means the two formulas are *not* equivalent. The Z3 model contains the counter example to provide to the student.
-2. `Unsat` -> Z3 proved that `P != Q` is not satisfiable, which means the two formulas are equivalent.
+1. `Sat` -> Z3 proved `P != Q` is satisfiable, which means that the formula `P == Q` is invalid. The Z3 model contains the counter example to provide to the student.
+2. `Unsat` -> Z3 proved that `P != Q` is not satisfiable, which means that the formula `P == Q` is valid.
 3. `Undef` -> Z3 was unable to decide the satisfiablity of `P != Q`. In this case we have to resort to other methods like QuickCheck to determine if the two formulas are equivalent or not.
 
 #### Notes
-- 
GitLab