mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

fix build on downlevel compilers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-21 09:12:10 -08:00
parent 98c5a779b4
commit 122a12c980
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -26,6 +26,8 @@ Notes:
#include"ast_pp.h" #include"ast_pp.h"
#include"lbool.h" #include"lbool.h"
const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
struct pb2bv_rewriter::imp { struct pb2bv_rewriter::imp {
@ -175,7 +177,6 @@ struct pb2bv_rewriter::imp {
         Niklas Een, Niklas Sörensson, JSAT 2006.          Niklas Een, Niklas Sörensson, JSAT 2006.
*/ */
const unsigned primes[7] = { 2, 3, 5, 7, 11, 13, 17};
vector<rational> m_min_base; vector<rational> m_min_base;
rational m_min_cost; rational m_min_cost;
@ -195,9 +196,9 @@ struct pb2bv_rewriter::imp {
m_min_base.push_back(delta_cost + rational::one()); 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<rational> seq1; vector<rational> seq1;
rational p(primes[i]); rational p(g_primes[i]);
rational rest = carry_in; rational rest = carry_in;
// create seq1 // create seq1
for (unsigned j = 0; j < seq.size(); ++j) { for (unsigned j = 0; j < seq.size(); ++j) {