From 5d74b862a390ccf4f2471fb8b9941314b4727c11 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Sun, 4 Mar 2018 14:41:27 +0100
Subject: This z3 option is necessary for good solving performance

---
 libsolidity/formal/Z3Interface.cpp | 1 +
 1 file changed, 1 insertion(+)

(limited to 'libsolidity')

diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 769e6edb..125da00d 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -28,6 +28,7 @@ using namespace dev::solidity::smt;
 Z3Interface::Z3Interface():
 	m_solver(m_context)
 {
+	z3::set_param("rewriter.pull_cheap_ite", true);
 }
 
 void Z3Interface::reset()
-- 
cgit