Skip to content

Commit 1fd8b87

Browse files
committed
Add header for magic numbers
All magic numbers throughout the codebase should eventually be added to this file.
1 parent c8f69b5 commit 1fd8b87

File tree

2 files changed

+14
-1
lines changed

2 files changed

+14
-1
lines changed

src/solvers/flattening/boolbv.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/symbol.h>
1616
#include <util/mp_arith.h>
1717
#include <util/arith_tools.h>
18+
#include <util/magic.h>
1819
#include <util/replace_expr.h>
1920
#include <util/std_types.h>
2021
#include <util/prefix.h>
@@ -688,7 +689,7 @@ bool boolbvt::is_unbounded_array(const typet &type) const
688689
return true;
689690

690691
if(unbounded_array==unbounded_arrayt::U_AUTO)
691-
if(s>1000) // magic number!
692+
if(s>MAX_FLATTENED_ARRAY_SIZE)
692693
return true;
693694

694695
return false;

src/util/magic.h

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
/// \file
2+
/// \brief Magic numbers used throughout the codebase
3+
/// \author Kareem Khazem <[email protected]>
4+
5+
#ifndef CPROVER_UTIL_MAGIC_H
6+
#define CPROVER_UTIL_MAGIC_H
7+
8+
#include <cstddef>
9+
10+
const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;
11+
12+
#endif

0 commit comments

Comments
 (0)