From 9de66957df6448ba1243cdb7cc84813fe82e69d5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 24 Aug 2012 00:29:52 +0000
Subject: fix get-value output in a couple ways; this fixes bug #378

---
 src/expr/node_manager.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/expr/node_manager.h')

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index bad20b3b6..18b60738f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -976,7 +976,7 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
 }
 
 inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
-  Assert(types.size() >= 2);
+  Assert(types.size() >= 1);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
     CheckArgument(!types[i].isFunctionLike(), types,
-- 
cgit v1.2.3