From f76f6bb0d969ffc27e9b7f6ddea78db5ee6fd876 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 1 Feb 2019 21:42:28 -0600
Subject: [PATCH] =?UTF-8?q?feat(solver):=20assert=20`true`=20and=20`=C2=AC?=
 =?UTF-8?q?false`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/smt/Solver.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml
index fe09716a..1f7a0e25 100644
--- a/src/smt/Solver.ml
+++ b/src/smt/Solver.ml
@@ -72,6 +72,12 @@ let create ?size ?(config=Config.empty) ~theories () : t =
   } in
   (* now add the theories *)
   Theory_combine.add_theory_l th_combine theories;
+  (* assert [true] and [not false] *)
+  let tst = tst self in
+  Sat_solver.assume self.solver [
+    [Lit.atom @@ Term.true_ tst];
+    [Lit.atom ~sign:false @@ Term.false_ tst];
+  ] Proof_default;
   self
 
 (** {2 Sat Solver} *)