cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Do not request proof for old z3

Browse Source
This commit is contained in:
Leonardo Alt 2020-12-03 19:16:04 +01:00
parent e04cc80438
commit 4210e09d9a
3 changed files with 20 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -15,6 +15,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1. * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1.
* SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals. * SMTChecker: Fix internal compiler error when doing bitwise compound assignment with string literals.
* SMTChecker: Fix internal error when trying to generate counterexamples with old z3.
* Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser. * Yul Optimizer: Fix a bug in NameSimplifier where a new name created by NameSimplifier could also be created by NameDispenser.
* Yul Optimizer: Removed NameSimplifier from optimization steps available to users. * Yul Optimizer: Removed NameSimplifier from optimization steps available to users.

22
libsmtutil/Z3CHCInterface.cpp
View File

@ -33,6 +33,13 @@ Z3CHCInterface::Z3CHCInterface(optional<unsigned> _queryTimeout):
m_context(m_z3Interface->context()), m_context(m_z3Interface->context()),
m_solver(*m_context) m_solver(*m_context)
{ {
Z3_get_version(
&get<0>(m_version),
&get<1>(m_version),
&get<2>(m_version),
&get<3>(m_version)
);
// These need to be set globally. // These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rewriter.pull_cheap_ite", true);
@ -73,7 +80,6 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr) pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
{ {
CheckResult result; CheckResult result;
CHCSolverInterface::CexGraph cex;
try try
{ {
z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr); z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
@ -82,9 +88,14 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
case z3::check_result::sat: case z3::check_result::sat:
{ {
result = CheckResult::SATISFIABLE; result = CheckResult::SATISFIABLE;
auto proof = m_solver.get_answer(); // z3 version 4.8.8 modified Spacer to also return
auto cex = cexGraph(proof); // proofs containing nonlinear clauses.
return {result, cex}; if (m_version >= tuple(4, 8, 8, 0))
{
auto proof = m_solver.get_answer();
return {result, cexGraph(proof)};
}
break;
} }
case z3::check_result::unsat: case z3::check_result::unsat:
{ {
@ -112,10 +123,9 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
result = CheckResult::UNKNOWN; result = CheckResult::UNKNOWN;
else else
result = CheckResult::ERROR; result = CheckResult::ERROR;
cex = {};
} }
return {result, cex}; return {result, {}};
} }
void Z3CHCInterface::setSpacerOptions(bool _preProcessing) void Z3CHCInterface::setSpacerOptions(bool _preProcessing)

3
libsmtutil/Z3CHCInterface.h
View File

@ -25,6 +25,7 @@
#include <libsmtutil/CHCSolverInterface.h> #include <libsmtutil/CHCSolverInterface.h>
#include <libsmtutil/Z3Interface.h> #include <libsmtutil/Z3Interface.h>
#include <tuple>
#include <vector> #include <vector>
namespace solidity::smtutil namespace solidity::smtutil
@ -64,6 +65,8 @@ private:
z3::context* m_context; z3::context* m_context;
// Horn solver. // Horn solver.
z3::fixedpoint m_solver; z3::fixedpoint m_solver;
std::tuple<unsigned, unsigned, unsigned, unsigned> m_version = std::tuple(0, 0, 0, 0);
}; };
} }