mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
disable automatic coersion to reals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4f33c123c9
commit
17984af4cc
|
@ -561,7 +561,8 @@ void arith_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
|
|||
if (logic == "NRA" ||
|
||||
logic == "QF_NRA" ||
|
||||
logic == "QF_UFNRA") {
|
||||
m_convert_int_numerals_to_real = true;
|
||||
// TBD: remove completely pending regressions:
|
||||
// m_convert_int_numerals_to_real = true;
|
||||
sort_names.push_back(builtin_name("Real", REAL_SORT));
|
||||
}
|
||||
else {
|
||||
|
|
Loading…
Reference in a new issue