Fix assertion from previous commit.

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 67e3fa0e9bb8f22760a57c38fd2835f7bb3d4bcd..964ea9c7372939d0ab97bf128704e9e4620e90e6 100644 (file)
--- 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