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

[SMTChecker] Do not throw when counterexample is not available (older z3 versions)

Browse Source
This commit is contained in:
Leonardo Alt 2020-09-23 16:51:52 +02:00
parent 858b4507e2
commit 5917fd82b3
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)
{
CexGraph graph;
/// The root fact of the refutation proof is `false`.
/// The node itself is not a hyper resolution, so we need to
/// extract the `query` hyper resolution node from the
/// `false` node (the first child).
smtAssert(_proof.is_app(), "");
smtAssert(fact(_proof).decl().decl_kind() == Z3_OP_FALSE, "");
/// The proof has the shape above for z3 >=4.8.8.
/// 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;
proofStack.push(_proof.arg(0));