From 93004a9d49effe79852fb19e48f545be56f37a73 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 6 May 2020 10:35:16 -0700
Subject: [PATCH] fix #4225

---
 src/nlsat/nlsat_solver.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 7488290256c..a7dbedca437 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -947,10 +947,13 @@ namespace nlsat {
         }
 
         void mk_clause(unsigned num_lits, literal const * lits, assumption a) {
-            SASSERT(num_lits > 0);
             _assumption_set as = nullptr;
             if (a != nullptr)
                 as = m_asm.mk_leaf(a);
+            if (num_lits == 0) {
+                num_lits = 1;
+                lits = &false_literal;
+            }
             mk_clause(num_lits, lits, false, as);
         }