From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Wed, 28 Apr 2010 20:19:29 +0000 (+0000)
Subject: SMT parser has to map 'Real' to RealType
X-Git-Tag: cvc5-1.0.0~9100
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b99ec8f0f659884d30c5fa1a9312addd07e75059;p=cvc5.git

SMT parser has to map 'Real' to RealType
---

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