SMT parser has to map 'Real' to RealType

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 48dc575a7e9ac1052ab0488bacdbe5e5812b9a78..6a34df3752678651c36af751c57b2c8ef75f9129 100644 (file)
--- 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);