mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

remove divergent ordering

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-05 17:18:24 +01:00
parent 23029daf5e
commit 8a420c850b
1 changed files with 0 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/asserted_formulas.cpp
View file

@ -556,14 +556,6 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
return false;
}
SASSERT(is_ground(lhs) && is_ground(rhs));
#if 0
if (is_uninterp_const(lhs) && is_app(rhs) && to_app(rhs)->get_num_args() > 0 && !occurs(lhs, rhs)) {
return true;
}
if (is_uninterp_const(rhs) && is_app(lhs) && to_app(lhs)->get_num_args() > 0 && !occurs(rhs, lhs)) {
return false;
}
#endif
if (depth(lhs) > depth(rhs)) {
return true;
}