From 122a12c980f211a474fae06f10353d398ea86bc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Feb 2017 09:12:10 -0800 Subject: [PATCH] fix build on downlevel compilers Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 24f9bf44b..b905ebff0 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -26,6 +26,8 @@ Notes: #include"ast_pp.h" #include"lbool.h" +const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17}; + struct pb2bv_rewriter::imp { @@ -175,7 +177,6 @@ struct pb2bv_rewriter::imp {          Niklas Een, Niklas Sörensson, JSAT 2006. */ - const unsigned primes[7] = { 2, 3, 5, 7, 11, 13, 17}; vector m_min_base; rational m_min_cost; @@ -195,9 +196,9 @@ struct pb2bv_rewriter::imp { m_min_base.push_back(delta_cost + rational::one()); } - for (unsigned i = 0; i < sizeof(primes)/sizeof(*primes); ++i) { + for (unsigned i = 0; i < sizeof(g_primes)/sizeof(*g_primes); ++i) { vector seq1; - rational p(primes[i]); + rational p(g_primes[i]); rational rest = carry_in; // create seq1 for (unsigned j = 0; j < seq.size(); ++j) {