From 44d533ad7e47daa636ee00a256b09fb3df9433ee Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 29 Apr 2019 20:52:18 +0100
Subject: 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.
---
 src/smtlib.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/smtlib.ml')

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
-- 
cgit v1.2.3