diff options
| author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-02 14:45:09 +0200 |
|---|---|---|
| committer | ajreynol <reynolds@larapc05.epfl.ch> | 2014-05-02 14:45:09 +0200 |
| commit | e0fa57b1d82647631984e01cbe700af39e348038 (patch) | |
| tree | 14c34c39f77598a88ca010c544a3b530784cf9b9 /src/theory/quantifiers/term_database.cpp | |
| parent | f625c0b8dbab3830198e6ad4ea9748cecd301389 (diff) | |
Fix assertion from previous commit.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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 |