fix #4106

Z3Prover · Apr 26, 2020 · 51c3778 · 51c3778
1 parent 530f772
commit 51c3778
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
@@ -306,9 +306,8 @@ struct check_logic::imp {
     }
 
     // check if the divisor is a numeral
-    void check_div(app * n) {
-        SASSERT(n->get_num_args() == 2);
-        if (!m_nonlinear && !is_numeral(n->get_arg(1)))
+    void check_div(app * n) {        
+        if (n->get_num_args() != 2 || (!m_nonlinear && !is_numeral(n->get_arg(1))))
             fail("logic does not support nonlinear arithmetic");
     }