mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
bc8ddedc54
commit
2a6b7e5482
|
@ -401,7 +401,6 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
|
|||
|
||||
app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
||||
if (is_int && !val.is_int()) {
|
||||
SASSERT(false);
|
||||
m_manager->raise_exception("invalid rational value passed as an integer");
|
||||
}
|
||||
if (val.is_unsigned()) {
|
||||
|
|
Loading…
Reference in a new issue