cerc-io/solidity
15
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 #9869 from ethereum/smt_fix_old_z3_cex

Browse Source 
[SMTChecker] Do not throw when counterexample is not available
This commit is contained in:
Alex Beregszaszi 2020-09-23 18:22:13 +01:00 committed by GitHub
commit a23e865645
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
libsmtutil/Z3CHCInterface.cpp
View File

@ -142,14 +142,17 @@ instead of a path.
*/ */
CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
{ {
CexGraph graph;
/// The root fact of the refutation proof is `false`. /// The root fact of the refutation proof is `false`.
/// The node itself is not a hyper resolution, so we need to /// The node itself is not a hyper resolution, so we need to
/// extract the `query` hyper resolution node from the /// extract the `query` hyper resolution node from the
/// `false` node (the first child). /// `false` node (the first child).
smtAssert(_proof.is_app(), ""); /// The proof has the shape above for z3 >=4.8.8.
smtAssert(fact(_proof).decl().decl_kind() == Z3_OP_FALSE, ""); /// If an older version is used, this check will fail and no
/// counterexample will be generated.
if (!_proof.is_app() || fact(_proof).decl().decl_kind() != Z3_OP_FALSE)
return {};
CexGraph graph;
stack<z3::expr> proofStack; stack<z3::expr> proofStack;
proofStack.push(_proof.arg(0)); proofStack.push(_proof.arg(0));