From 9223f611ba6748c5e36d67c2e7d7dcc28ad4b4ff Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Apr 2020 14:49:27 -0700
Subject: [PATCH] build

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

diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 2199c46c0..f0692ae57 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -814,6 +814,8 @@ theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
 
 template<typename Ext>
 void theory_diff_logic<Ext>::set_sort(expr* n) {
+    if (m_util.is_numeral(n))
+        return;
     if (m_util.is_int(n)) {
         if (m_lia_or_lra == is_lra) {
             throw default_exception("difference logic does not work with mixed sorts");