From b99ec8f0f659884d30c5fa1a9312addd07e75059 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Wed, 28 Apr 2010 20:19:29 +0000
Subject: [PATCH] SMT parser has to map 'Real' to RealType

---
 src/parser/smt/Smt.g | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);
-- 
2.30.2