From 1d6fb6352fb5def39a2ca30ef9602246b34bc979 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 21:00:52 -0700
Subject: [PATCH] fix #3631

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 7f4e290c0..f1bd9c749 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2076,12 +2076,20 @@ namespace sat {
             else 
                 polarity = polarity ^ sign;
         }
-        if (lits.empty()) {
-            throw default_exception("empty xor is TBD");
-        }
-        if (polarity) {
+        if (polarity && !lits.empty()) {
             lits[0].neg();
         }
+        switch (lits.size()) {
+        case 0:
+            if (polarity)
+                s().set_conflict(justification(0));
+            return nullptr;
+        case 1:            
+            s().assign_scoped(lits[0]);
+            return nullptr;
+        default:
+            break;
+        }
         void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
         xr* x = new (mem) xr(next_id(), lits);
         x->set_learned(learned);