mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

#5532

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-21 20:21:23 -07:00
parent 18d1b368d1
commit d174f87c5e
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/subpaving/tactic/expr2subpaving.cpp
View file

@ -19,9 +19,10 @@ Notes:
--*/
#include "math/subpaving/tactic/expr2subpaving.h"
#include "ast/expr2var.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
#include "util/ref_util.h"
#include "util/z3_exception.h"
#include "ast/arith_decl_plugin.h"
#include "util/scoped_numeral_buffer.h"
#include "util/common_msgs.h"
@ -309,6 +310,10 @@ struct expr2subpaving::imp {
case OP_MOD:
case OP_REM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
case OP_DIV0:
case OP_REM0:
case OP_MOD0:
case OP_IDIV0:
throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module.");
case OP_SIN:
case OP_COS:
@ -325,6 +330,7 @@ struct expr2subpaving::imp {
// TODO
throw default_exception("transcendental and hyperbolic functions are not supported yet.");
default:
throw default_exception("unhandled arithmetic operator in subpaving");
UNREACHABLE();
}
return subpaving::null_var;