summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/parser/CMakeLists.txt1
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp3
2 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 2fe92fb45..3fccac37b 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -8,7 +8,6 @@
## All rights reserved. See the file COPYING in the top-level source
## directory for licensing information.
##
-set(ANTLR_HOME ${ANTLR_DIR})
find_package(ANTLR REQUIRED)
if(NOT HAVE_ANTLR3_FILE_STREAM_NEW)
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