mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
disable case1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d80e2fb61d
commit
f014e30d46
|
@ -596,7 +596,7 @@ namespace opt {
|
|||
bool use_case1 = abs_src_c == abs_dst_c && src_c.is_pos() != dst_c.is_pos() && !abs_src_c.is_one() && t_le == dst.m_type && t_le == src.m_type;
|
||||
bool use_case2 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one();
|
||||
|
||||
if (use_case1) {
|
||||
if (use_case1 && false) {
|
||||
//
|
||||
// x*src_c + s <= 0
|
||||
// -x*src_c + t <= 0
|
||||
|
|
Loading…
Reference in a new issue