From 3d4d23691c33ea439dfbf7b4b1038b704f1003d5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 May 2017 15:58:13 +0200 Subject: [PATCH] fixed translation of mathsat's rational number expressions to storm's rational number expressions --- src/storm/adapters/MathsatExpressionAdapter.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index 63edcc371..1e70d546a 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -13,6 +13,7 @@ #include "storage/expressions/Expressions.h" #include "storage/expressions/ExpressionVisitor.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/ExpressionEvaluationException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -250,10 +251,13 @@ namespace storm { msat_free(name); return result; } else if (msat_term_is_number(env, term)) { + char* termAsCString = msat_term_repr(term); + std::string termString(termAsCString); + msat_free(termAsCString); if (msat_is_integer_type(env, msat_term_get_type(term))) { return manager.integer(std::stoll(msat_term_repr(term))); } else if (msat_is_rational_type(env, msat_term_get_type(term))) { - return manager.rational(std::stod(msat_term_repr(term))); + return manager.rational(storm::utility::convertNumber(termString)); } }