From 51c3778354b3b960edf076b927af99c36208a661 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2020 14:55:12 -0700 Subject: [PATCH] fix #4106 --- src/cmd_context/check_logic.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index c9cc88556..1c3101e25 100644 --- 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"); }