summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-03-02 00:26:29 -0800
committerGitHub <noreply@github.com>2021-03-02 08:26:29 +0000
commit0d5ab1705324e91d9788185cd16e1d4e6bf54fbe (patch)
tree3480e9df08b5a6d250a1e19d96fc7142702eb018 /src/theory
parent968ba63bab1709096f09efcdf84651c8c1481110 (diff)
Add aarch64 (ARM64) cross-compile support. (#6033)
This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64. Fixes #1479 #5769.
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index fb0505bae..1b7355fdf 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -788,7 +788,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
{
long rr = range.getConst<Rational>().getNumerator().getLong()+1;
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
- for( unsigned k=0; k<rr; k++ ){
+ for (long k = 0; k < rr; k++)
+ {
Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) );
t = Rewriter::rewrite( t );
elements.push_back( t );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback