From b88b906da991ef0f948f16143e3642eef52e95fc Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 21 Nov 2016 15:51:55 +0100
Subject: [PATCH] Added test for bug (conflict at level 0)

---
 tests/test_api.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/tests/test_api.ml b/tests/test_api.ml
index 75ae7fd2..346e483e 100644
--- a/tests/test_api.ml
+++ b/tests/test_api.ml
@@ -144,6 +144,18 @@ module Test = struct
       solve `Expect_unsat;
     ] |> mk_test "test3"
 
+  (* Conflict at level 0 *)
+  let test4 =
+    [ assume [[-1; -2]];
+      solve `Expect_sat;
+      assume [[1]];
+      solve `Expect_sat;
+      assume [[2]];
+      solve ~assumptions:[3] `Expect_unsat;
+      solve ~assumptions:[] `Expect_unsat;
+      solve ~assumptions:[] `Expect_unsat;
+    ] |> mk_test "conflict0"
+
   (* just check that we do create new solvers *)
   let test_clean =
     [ solve `Expect_sat
@@ -153,6 +165,7 @@ module Test = struct
     [ test1;
       test2;
       test3;
+      test4;
       test_clean; (* after test3 *)
     ]
 end