diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:32 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-13 14:12:41 +0100 |
| commit | 82fbac8829cbc41927216b36ab064b50e50b2fa0 (patch) | |
| tree | 346361d002c109b8ac2254f4f215a12dfc7643d2 /src/theory/quantifiers | |
| parent | 3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9 (diff) | |
Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 616c51f54..f9c8e42fd 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -528,7 +528,7 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { for( unsigned k=0; k<vars[lhs].size(); k++ ){ int v = vars[lhs][k]; Trace("cegqi-si-debug") << " variable " << v << std::endl; - Assert( vars[lhs].size()==vn ); + Assert( (int)vars[lhs].size()==vn ); //check if already processed bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end(); if( proc==(p==1) ){ |