diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,11 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.8.0 _(2024-11-28)_
+
+### Changed
+- Replaced representation of `RealSort` values in Haskell with `Rational` instead of `Double`
+
 ## v2.7.2 _(2024-11-27)_
 
 ### Added
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.7.2
+version:               2.8.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -137,15 +137,15 @@
   decode sol (Or x y)           = (||) <$> decode sol x <*> decode sol y
   decode sol (Impl x y)         = (==>) <$> decode sol x <*> decode sol y
   decode sol (Xor x y)          = xor   <$> decode sol x <*> decode sol y
-  decode _ Pi                   = Just pi
-  decode sol (Sqrt x)           = fmap sqrt  (decode sol x)
-  decode sol (Exp x)            = fmap exp   (decode sol x)
-  decode sol (Sin x)            = fmap sin   (decode sol x)
-  decode sol (Cos x)            = fmap cos   (decode sol x)
-  decode sol (Tan x)            = fmap tan   (decode sol x)
-  decode sol (Asin x)           = fmap asin  (decode sol x)
-  decode sol (Acos x)           = fmap acos  (decode sol x)
-  decode sol (Atan x)           = fmap atan  (decode sol x)
+  decode _ Pi                   = Just $ toRational pi
+  decode sol (Sqrt x)           = fmap (toRational . sqrt . fromRational @Double)  (decode sol x)
+  decode sol (Exp x)            = fmap (toRational . exp . fromRational @Double)   (decode sol x)
+  decode sol (Sin x)            = fmap (toRational . sin . fromRational @Double)   (decode sol x)
+  decode sol (Cos x)            = fmap (toRational . cos . fromRational @Double)   (decode sol x)
+  decode sol (Tan x)            = fmap (toRational . tan . fromRational @Double)   (decode sol x)
+  decode sol (Asin x)           = fmap (toRational . asin . fromRational @Double)  (decode sol x)
+  decode sol (Acos x)           = fmap (toRational . acos . fromRational @Double)  (decode sol x)
+  decode sol (Atan x)           = fmap (toRational . atan . fromRational @Double)  (decode sol x)
   decode sol (ToReal x)         = fmap realToFrac (decode sol x)
   decode sol (ToInt x)          = fmap truncate   (decode sol x)
   decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -167,7 +167,7 @@
 constant :: forall t. KnownSMTSort t => Parser (HaskellType t)
 constant = case sortSing @t of
   SIntSort       -> anyValue decimal
-  SRealSort      -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational
+  SRealSort      -> anyValue parseRational <|> parseToRealRational <|> anyValue rational
   SBoolSort      -> parseBool
   SBvSort _ p    -> anyBitvector p
   SArraySort k v -> constArray k v
@@ -288,25 +288,25 @@
   return $ negate val
 {-# INLINE negativeValue #-}
 
-parseRatioDouble :: Parser Double
-parseRatioDouble = do
+parseRational :: Parser Rational
+parseRational = do
   _           <- char '(' >> skipSpace >> char '/' >> skipSpace
   numerator   <- decimal
   _           <- skipSpace
   denominator <- decimal
   _           <- skipSpace >> char ')'
 
-  return $ fromRational $ numerator % denominator
-{-# INLINEABLE parseRatioDouble #-}
+  return $ numerator % denominator
+{-# INLINEABLE parseRational #-}
 
-parseToRealDouble :: Parser Double
-parseToRealDouble = do
+parseToRealRational :: Parser Rational
+parseToRealRational = do
   _   <- char '(' >> skipSpace >> string "to_real" >> skipSpace
   dec <- anyValue decimal
   _   <- skipSpace >> char ')'
 
-  return $ fromInteger dec
-{-# INLINEABLE parseToRealDouble #-}
+  return $ toRational dec
+{-# INLINEABLE parseToRealRational #-}
 
 parseBool :: Parser Bool
 parseBool = (string "true" *> pure True) <|> (string "false" *> pure False)
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -10,6 +10,7 @@
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.ArrayMap
+import Data.Ratio
 import Data.Coerce
 import Data.Some.Constraint
 import Data.Sequence
@@ -64,6 +65,14 @@
     | x < 0     = "(- " <> formatDouble standardDefaultPrecision (abs x) <> ")"
     | otherwise = formatDouble standardDefaultPrecision x
   {-# INLINE render #-}
+
+instance Render Rational where
+  render x = if num < 0
+             then "(/ " <> "(- " <> render (abs num) <> ") " <> render denom <> ")"
+             else "(/ " <> render num <> " " <> render denom <> ")"
+    where
+      num = numerator x
+      denom = denominator x
 
 instance Render Char where
   render = char8
diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs
--- a/src/Language/Hasmtlib/Type/SMTSort.hs
+++ b/src/Language/Hasmtlib/Type/SMTSort.hs
@@ -44,7 +44,7 @@
 -- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.
 type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
   HaskellType IntSort         = Integer
-  HaskellType RealSort        = Double
+  HaskellType RealSort        = Rational
   HaskellType BoolSort        = Bool
   HaskellType (BvSort enc n)  = Bitvec enc n
   HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)