From 8a420c850bcbb69a1f13f781b29db8ae2bfb7db3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Nov 2019 17:18:24 +0100 Subject: [PATCH] remove divergent ordering Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index a08ef09af..3db9dc172 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -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; }