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

Merge pull request #10493 from ethereum/smt_fix_487

Browse Source 
[SMTChecker] Do not request proof for old z3
This commit is contained in:
Leonardo 2020-12-03 22:17:41 +01:00 committed by GitHub
commit a27d7707c8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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:
* 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 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: 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_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.
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)
{
CheckResult result;
CHCSolverInterface::CexGraph cex;
try
{
z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
@ -82,9 +88,14 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
case z3::check_result::sat:
{
result = CheckResult::SATISFIABLE;
auto proof = m_solver.get_answer();
auto cex = cexGraph(proof);
return {result, cex};
// z3 version 4.8.8 modified Spacer to also return
// proofs containing nonlinear clauses.
if (m_version >= tuple(4, 8, 8, 0))
{
auto proof = m_solver.get_answer();
return {result, cexGraph(proof)};
}
break;
}
case z3::check_result::unsat:
{
@ -112,10 +123,9 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
cex = {};
}
return {result, cex};
return {result, {}};
}
void Z3CHCInterface::setSpacerOptions(bool _preProcessing)

3
libsmtutil/Z3CHCInterface.h
View File

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