fix #2706

NikolajBjorner · NikolajBjorner · commit cbac8603873a · 2019-11-16T09:06:58.000-08:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git 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)) {

Original file line number	Diff line number	Diff line change
`@@ -372,8 +372,6 @@ namespace smt {`
`372`	`372`	`if (_val.is_zero()) {`
`373`	`373`	`return internalize_numeral(m, val);`
`374`	`374`	`}`
`375`		`- SASSERT(!val.is_zero());`
`376`		`- SASSERT(!val.is_one());`
`377`	`375`	`unsigned r_id = mk_row();`
`378`	`376`	`scoped_row_vars _sc(m_row_vars, m_row_vars_top);`
`379`	`377`	`if (is_var(arg1)) {`