diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-06-03 19:56:12 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-06-03 19:56:12 +0000 |
| commit | daa163e694d257ffe8ba7ae8ccb240bcbfb1c276 (patch) | |
| tree | be974acd22bdb38cd0f8693d83ec99469a33866e /src/parser/cvc | |
| parent | 4a696409769044ad155a56eeb00c9d85246ca0b4 (diff) | |
fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d6165b435..cd4c66664 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1467,7 +1467,7 @@ postfixTerm[CVC4::Expr& f] Expr e = f.getOperator(); const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator()[0] )); + MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() )); v.insert(v.end(), f.begin(), f.end()); f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); } else { |