aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLeonardo Alt <leonardoaltt@gmail.com>2018-03-04 21:41:27 +0800
committerLeonardo Alt <leonardoaltt@gmail.com>2018-03-04 21:42:36 +0800
commit5d74b862a390ccf4f2471fb8b9941314b4727c11 (patch)
treedcef58efe3fd225f74188a9de8bfd1b45c696ff0
parent7e2f3d3e0727cf6ef8779abd3cf6e00e5332f1ef (diff)
downloaddexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.tar
dexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.tar.gz
dexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.tar.bz2
dexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.tar.lz
dexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.tar.xz
dexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.tar.zst
dexon-solidity-5d74b862a390ccf4f2471fb8b9941314b4727c11.zip
This z3 option is necessary for good solving performance
-rw-r--r--libsolidity/formal/Z3Interface.cpp1
1 files changed, 1 insertions, 0 deletions
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()