Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

4 files changed, 63 insertions, 59 deletions

diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index c89005941..31a2219b9 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -133,70 +133,71 @@ antlr3CommonTokenDebugStreamSourceNew(ANTLR3_UINT32 hint, pANTLR3_TOKEN_SOURCE s
 	return stream;
 }*/
 
-pBOUNDED_TOKEN_BUFFER
-BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pANTLR3_TOKEN_SOURCE source)
-{
-    pBOUNDED_TOKEN_BUFFER buffer;
-    pANTLR3_COMMON_TOKEN_STREAM	stream;
-
-
-    assert( k > 0 );
+pBOUNDED_TOKEN_BUFFER BoundedTokenBufferSourceNew(ANTLR3_UINT32 k,
+                                                  pANTLR3_TOKEN_SOURCE source) {
+  pBOUNDED_TOKEN_BUFFER buffer;
+  pANTLR3_COMMON_TOKEN_STREAM stream;
 
-    /* Memory for the interface structure
-     */
-    buffer = (pBOUNDED_TOKEN_BUFFER) ANTLR3_MALLOC(sizeof(BOUNDED_TOKEN_BUFFER_struct));
+  assert(k > 0);
 
-    if	(buffer == NULL)
-    {
-	return	NULL;
-    }
+  /* Memory for the interface structure */
+  buffer =
+      (pBOUNDED_TOKEN_BUFFER)ANTLR3_MALLOC(sizeof(BOUNDED_TOKEN_BUFFER_struct));
 
-    buffer->tokenBuffer = (pANTLR3_COMMON_TOKEN*) ANTLR3_MALLOC(2*k*sizeof(pANTLR3_COMMON_TOKEN));
-    buffer->currentIndex = 0;
-    buffer->maxIndex = 0;
-    buffer->k = k;
-    buffer->bufferSize = 2*k;
-    buffer->empty = ANTLR3_TRUE;
-    buffer->done = ANTLR3_FALSE;
-
-    stream = antlr3CommonTokenStreamSourceNew(k,source);
-    if  (stream == NULL)
-    {
-        return  NULL;
-    }
+  if (buffer == NULL) {
+    return NULL;
+  }
 
-    stream->super = buffer;
-    buffer->commonTstream = stream;
+  buffer->tokenBuffer = (pANTLR3_COMMON_TOKEN*)ANTLR3_MALLOC(
+      2 * k * sizeof(pANTLR3_COMMON_TOKEN));
+  if (buffer->tokenBuffer == NULL) {
+    ANTLR3_FREE(buffer);
+    return NULL;
+  }
 
-    /* Defaults
-     */
-    stream->p	    = -1;
+  buffer->currentIndex = 0;
+  buffer->maxIndex = 0;
+  buffer->k = k;
+  buffer->bufferSize = 2 * k;
+  buffer->empty = ANTLR3_TRUE;
+  buffer->done = ANTLR3_FALSE;
+
+  stream = antlr3CommonTokenStreamSourceNew(k, source);
+  if (stream == NULL) {
+    ANTLR3_FREE(buffer->tokenBuffer);
+    ANTLR3_FREE(buffer);
+    return NULL;
+  }
 
-    /* Install the token stream API
-     */
-    stream->tstream->_LT				=  tokLT;
-    stream->tstream->get				=  get;
-    stream->tstream->getTokenSource		=  getTokenSource;
-    stream->tstream->setTokenSource		=  setTokenSource;
-    stream->tstream->toString			=  toString;
-    stream->tstream->toStringSS			=  toStringSS;
-    stream->tstream->toStringTT			=  toStringTT;
-	stream->tstream->setDebugListener	=  setDebugListener;
-
-    /* Install INT_STREAM interface
-     */
-    stream->tstream->istream->_LA	=  _LA;
-    stream->tstream->istream->mark	=  mark;
-    stream->tstream->istream->release	=  release;
-    stream->tstream->istream->size	=  size;
-    stream->tstream->istream->index	=  tindex;
-    stream->tstream->istream->rewind	=  rewindStream;
-    stream->tstream->istream->rewindLast=  rewindLast;
-    stream->tstream->istream->seek	=  seek;
-    stream->tstream->istream->consume	=  consume;
-    stream->tstream->istream->getSourceName = getSourceName;
-
-    return  buffer;
+  stream->super = buffer;
+  buffer->commonTstream = stream;
+
+  /* Defaults */
+  stream->p = -1;
+
+  /* Install the token stream API */
+  stream->tstream->_LT = tokLT;
+  stream->tstream->get = get;
+  stream->tstream->getTokenSource = getTokenSource;
+  stream->tstream->setTokenSource = setTokenSource;
+  stream->tstream->toString = toString;
+  stream->tstream->toStringSS = toStringSS;
+  stream->tstream->toStringTT = toStringTT;
+  stream->tstream->setDebugListener = setDebugListener;
+
+  /* Install INT_STREAM interface */
+  stream->tstream->istream->_LA = _LA;
+  stream->tstream->istream->mark = mark;
+  stream->tstream->istream->release = release;
+  stream->tstream->istream->size = size;
+  stream->tstream->istream->index = tindex;
+  stream->tstream->istream->rewind = rewindStream;
+  stream->tstream->istream->rewindLast = rewindLast;
+  stream->tstream->istream->seek = seek;
+  stream->tstream->istream->consume = consume;
+  stream->tstream->istream->getSourceName = getSourceName;
+
+  return buffer;
 }
 
 // Install a debug listener adn switch to debug mode methods
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index c9515aa92..1554428f7 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -110,6 +110,7 @@ static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input,
 
   input->data = mmap(0, input->sizeBuf, PROT_READ, MAP_PRIVATE, fd, 0);
   errno = 0;
+  close(fd);
   if(intptr_t(input->data) == -1) {
     return ANTLR3_ERR_NOMEM;
   }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 29d3e45b6..f88b30212 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1610,7 +1610,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) {
         //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
         //However, the expression has 0 children. So we convert to a SEP_NIL variable.
-        expr = EXPR_MANAGER->mkSepNil(type);
+        expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL);
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9f3c43f09..30573cdff 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -372,6 +372,8 @@ void Smt2::setLogic(std::string name) {
       name = "UFBV";
     } else if(name == "SLIA") {
       name = "UFSLIA";
+    } else if(name == "SAT") {
+      name = "UF";
     } else if(name == "ALL_SUPPORTED") {
       //no change
     } else {