From 345c0f36fb63990b27ddd9c82385a60b2276bd04 Mon Sep 17 00:00:00 2001
From: chriseth <c@ethdev.com>
Date: Sat, 20 Aug 2016 03:44:26 +0200
Subject: Fix crash when using json compiler with exponentiation.

---
 libsolidity/formal/Why3Translator.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'libsolidity/formal')

diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index bd0a020d..e16c41ab 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -466,7 +466,8 @@ bool Why3Translator::visit(BinaryOperation const& _binaryOperation)
 		auto const& constantNumber = dynamic_cast<RationalNumberType const&>(commonType);
 		if (constantNumber.isFractional())
 			error(_binaryOperation, "Fractional numbers not supported.");
-		add("(of_int " + toString(commonType.literalValue(nullptr)) + ")");
+		else
+			add("(of_int " + toString(commonType.literalValue(nullptr)) + ")");
 		return false;
 	}
 	static const map<Token::Value, char const*> optrans({
@@ -488,7 +489,10 @@ bool Why3Translator::visit(BinaryOperation const& _binaryOperation)
 		{Token::GreaterThanOrEqual, " >= "}
 	});
 	if (!optrans.count(c_op))
+	{
 		error(_binaryOperation, "Operator not supported.");
+		return true;
+	}
 
 	add("(");
 	leftExpression.accept(*this);
@@ -676,7 +680,8 @@ bool Why3Translator::visit(Literal const& _literal)
 		auto const& constantNumber = dynamic_cast<RationalNumberType const&>(*type);
 		if (constantNumber.isFractional())
 			error(_literal, "Fractional numbers not supported.");
-		add("(of_int " + toString(type->literalValue(&_literal)) + ")");
+		else
+			add("(of_int " + toString(type->literalValue(&_literal)) + ")");
 		break;
 	}	
 	default:
-- 
cgit v1.2.3