mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3a26dccc8a
commit
293b0b8cc2
|
@ -1251,7 +1251,6 @@ namespace smt {
|
|||
expr * rhs2;
|
||||
if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); }
|
||||
if (!m_util.is_numeral(rhs)) {
|
||||
SASSERT(false);
|
||||
throw default_exception("malformed atomic constraint");
|
||||
}
|
||||
theory_var v = internalize_term_core(lhs);
|
||||
|
|
Loading…
Reference in a new issue