fix hgoes#20

jwaldmann · Mar 16, 2021 · f96e515 · f96e515
1 parent f1f1146
commit f96e515
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/backends/pipe/Language/SMTLib2/Pipe/Internals.hs b/backends/pipe/Language/SMTLib2/Pipe/Internals.hs
@@ -769,7 +769,10 @@ lispToExprWith :: (GShow fun,GShow e,GetFunType fun,GetType e)
                    -> LispParse a)
                -> LispParse a
 lispToExprWith p hint (runExcept . lispToConstant -> Right (AnyValue val)) res
-  = res (Const val)
+  = case (hint,val) of
+      (Just (Sort RealRepr), IntValue i) ->
+        res (Const $ RealValue $ fromInteger i)
+      _ -> res (Const val)
 lispToExprWith p hint (L.Symbol sym) res
   = parseVar p hint sym (res . Expr.Var) (res . Expr.QVar) (res . Expr.FVar) (res . Expr.LVar) `catchError`
     (\_ -> do