diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-28 20:19:29 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-28 20:19:29 +0000 |
| commit | b99ec8f0f659884d30c5fa1a9312addd07e75059 (patch) | |
| tree | 3e9455b41bb97bd96eda8cd3ef26647198376e52 | |
| parent | c59fe5b21c218d3d6048cc5c34a7e27b3643ae78 (diff) | |
SMT parser has to map 'Real' to RealType
| -rw-r--r-- | src/parser/smt/Smt.g | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 48dc575a7..6a34df375 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -93,7 +93,7 @@ setLogic(Parser *parser, const std::string& name) { if( name == "QF_UF" ) { parser->mkSort("U"); } else if(name == "QF_LRA"){ - parser->mkSort("Real"); + parser->defineType("Real", parser->getExprManager()->realType()); } else{ // NOTE: Theory types go here Unhandled(name); |