diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:05:23 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-16 14:05:23 -0500 |
| commit | 00785f2b65eb9dfdfbfcd8b58b0cc57255919c31 (patch) | |
| tree | 3e737a65502c2633d525b4d7344a3ae6f9a3c2ed /src/parser | |
| parent | 46857bda6c6bb6db3481514c8cdee3ecbadb3301 (diff) | |
Minor fixes, always expand applications of lambdas at preprocess.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bb7ac9fb8..c52f2ad51 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2074,10 +2074,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] if( !type.isConstructor() ){ PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); } - //TODO - //if( Datatype::datatypeOf(f).isParametric() ){ - // type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); - //} + if( Datatype::datatypeOf(f).isParametric() ){ + type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType()); + } match_ptypes = ((ConstructorType)type).getArgTypes(); } //arguments |