SMT: Refactor overflow checks into generic event checking system

Have assert events for assertions and overflow events for potential
integer overflow. Unclear how these should interact... The order in
which such events are applied to the final assertion is potentially
quite important.

Overflow checks and assertions are now path sensitive, as they should
be.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/smtlib.ml b/src/smtlib.ml
index 3ba85306..fe7aee5e 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -124,12 +124,16 @@ let bvones n =
 
 let simp_fn = function
   | Fn ("not", [Fn ("not", [exp])]) -> exp
+  | Fn ("not", [Bool_lit b]) -> Bool_lit (not b)
   | Fn ("contents", [Fn ("Bits", [_; contents])]) -> contents
   | Fn ("len", [Fn ("Bits", [len; _])]) -> len
+  | Fn ("or", [x]) -> x
+  | Fn ("and", [x]) -> x
   | exp -> exp
 
 let simp_ite = function
   | Ite (cond, Bool_lit true, Bool_lit false) -> cond
+  | Ite (cond, Bool_lit x, Bool_lit y) when x = y -> Bool_lit x
   | Ite (_, Var v, Var v') when v = v' -> Var v
   | Ite (Bool_lit true, then_exp, _) -> then_exp
   | Ite (Bool_lit false, _, else_exp) -> else_exp