From d231a82837ffe4d3660f198d2495a7ea200fa838 Mon Sep 17 00:00:00 2001 From: shellygr Date: Thu, 4 Jan 2024 13:07:32 +0200 Subject: [PATCH] Update builtin.md --- docs/cvl/builtin.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/cvl/builtin.md b/docs/cvl/builtin.md index 098fe022..17c2c6a3 100644 --- a/docs/cvl/builtin.md +++ b/docs/cvl/builtin.md @@ -106,11 +106,11 @@ rule sanity { method f; env e; calldataarg arg; f(e, arg); - assert false; + satisfy true; } ``` -To find a counterexample to the assertion, the Prover must construct an input +To find a satisfying trace, the Prover must construct an input for which `f` doesn't revert. (built-in-deep-sanity)=