From: ajreynol <reynolds@larapc05.epfl.ch>
Date: Fri, 2 May 2014 12:45:09 +0000 (+0200)
Subject: Fix assertion from previous commit.
X-Git-Tag: cvc5-1.0.0~6935
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0fa57b1d82647631984e01cbe700af39e348038;p=cvc5.git

Fix assertion from previous commit.
---

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