From 0f7bebcbed8fe33c6d5c3f9c653be57eb7e9adb8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Dec 2022 09:49:32 -0800 Subject: [PATCH] try big M for linux build --- src/ast/rewriter/poly_rewriter.h | 1 + src/ast/rewriter/poly_rewriter_def.h | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index c9253b0e4..6880f7e23 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -36,6 +36,7 @@ protected: bool m_hoist_mul; bool m_ast_order; bool m_hoist_ite; + ast_manager& M() { return Config::m; } bool is_numeral(expr * n) const { return Config::is_numeral(n); } bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); } diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index f9ae333b4..33f1b510a 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -51,7 +51,7 @@ expr * poly_rewriter::mk_add_app(unsigned num_args, expr * const * args) switch (num_args) { case 0: return mk_numeral(numeral(0)); case 1: return args[0]; - default: return m.mk_app(get_fid(), add_decl_kind(), num_args, args); + default: return M().mk_app(get_fid(), add_decl_kind(), num_args, args); } }