From cb21f70cc3111091be9098a4249157736b21a08a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 20 Dec 2019 15:42:03 -0800
Subject: [PATCH] fix #2813

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.h      |  2 +-
 src/smt/theory_arith_int.h | 17 ++++++++++++-----
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 0b78bc887..86e2a27cb 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -956,7 +956,7 @@ namespace smt {
 
     public:
         void assign(literal l, const b_justification & j, bool decision = false) {
-            SASSERT(l != false_literal);
+            // SASSERT(l != false_literal);
             SASSERT(l != null_literal);
             switch (get_assignment(l)) {
             case l_false:
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index ffbb9770d..8d300f8aa 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -667,11 +667,18 @@ namespace smt {
         l = ctx.get_literal(bound);
         ctx.mark_as_relevant(l);
         dump_lemmas(l, ante);
-        ctx.assign(l, ctx.mk_justification(
-                       gomory_cut_justification(
-                           get_id(), ctx.get_region(), 
-                           ante.lits().size(), ante.lits().c_ptr(), 
-                           ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
+        auto js = ctx.mk_justification(
+            gomory_cut_justification(
+                get_id(), ctx.get_region(),
+                ante.lits().size(), ante.lits().c_ptr(),
+                ante.eqs().size(), ante.eqs().c_ptr(), ante, l));
+
+        if (l == false_literal) {
+            ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA, nullptr);
+        }
+        else {
+            ctx.assign(l, js);
+        }
         return true;
     }