From e0fa57b1d82647631984e01cbe700af39e348038 Mon Sep 17 00:00:00 2001
From: ajreynol <reynolds@larapc05.epfl.ch>
Date: Fri, 2 May 2014 14:45:09 +0200
Subject: [PATCH] Fix assertion from previous commit.

---
 src/theory/quantifiers/term_database.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 67e3fa0e9..964ea9c73 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -516,7 +516,7 @@ Node TermDb::getSkolemizedBody( Node f ){
     std::vector< TypeNode > fvTypes;
     std::vector< TNode > fvs;
     d_skolem_body[ f ] = mkSkolemizedBody( f, f[1], fvTypes, fvs, d_skolem_constants[f] );
-    Assert( d_skolem_constants.size()==f[0].getNumChildren() );
+    Assert( d_skolem_constants[f].size()==f[0].getNumChildren() );
     if( options::sortInference() ){
       for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
         //carry information for sort inference
-- 
2.30.2