From cbac8603873a3d4b3117ea9f5aef5fc150e31076 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 16 Nov 2019 09:06:54 -0800
Subject: [PATCH] fix #2706

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

diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 39bcb0e02..ceb07eafa 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -372,8 +372,6 @@ namespace smt {
             if (_val.is_zero()) {
                 return internalize_numeral(m, val);
             }
-            SASSERT(!val.is_zero());
-            SASSERT(!val.is_one());
             unsigned r_id = mk_row();
             scoped_row_vars _sc(m_row_vars, m_row_vars_top);
             if (is_var(arg1)) {