From 2bba885266c63a1ecfaaeef371a07d95e3877e96 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 24 Jul 2018 23:42:20 +0200
Subject: [PATCH] Prevent semantic propagations at level 0

---
 src/core/internal.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 0409fb19..d501ed67 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -568,6 +568,10 @@ module Make
     else match Plugin.eval a.lit with
       | Plugin_intf.Unknown -> None
       | Plugin_intf.Valued (b, l) ->
+        if l = [] then
+          raise (Invalid_argument (
+              Format.asprintf "msat:core/internal.ml: %s"
+                "semantic propagation at level 0 are currently forbidden"));
         let atom = if b then a else a.neg in
         enqueue_semantic atom l;
         Some b