From 1da64bfe4cc9311a47686546d48452c595710299 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Feb 2020 21:40:52 -1000
Subject: [PATCH] fix #3019

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/subpaving/subpaving_t_def.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index 91ff9833b..c74c058e9 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -1777,6 +1777,8 @@ void context_t<C>::assert_units(node * n) {
         ineq * a = UNTAG(ineq*, *it);
         bool axiom = GET_TAG(*it) != 0;
         TRACE("subpaving_init", tout << "asserting: "; display(tout, a); tout << ", axiom: " << axiom << "\n";);
+        if (a->x() == null_var)
+            continue;
         propagate_bound(a->x(), a->value(), a->is_lower(), a->is_open(), n, justification(axiom));
         if (inconsistent(n))
             break;