From b0a47ca897b289afd5b3629237020271bcfc707f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Mar 2017 08:11:38 -0800 Subject: [PATCH] disable pb sorting Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index b905ebff0..1afb56c1a 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -112,13 +112,14 @@ struct pb2bv_rewriter::imp { return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m); } +#if 0 expr_ref result(m); switch (is_le) { case l_true: if (mk_le(sz, args, k, result)) return result; else break; case l_false: if (mk_ge(sz, args, k, result)) return result; else break; case l_undef: if (mk_eq(sz, args, k, result)) return result; else break; } - +#endif // fall back to divide and conquer encoding. SASSERT(k.is_pos()); expr_ref zero(m), bound(m);