From cb4ffbfbb7509191483834972ee5c504f7908f08 Mon Sep 17 00:00:00 2001 From: david-k Date: Fri, 4 Mar 2022 11:02:54 +0100 Subject: [PATCH] Fix leftover use of divModWithSlacks in doc The option `divModWithSlacks` was previously changed to `divModNoSlacks`. However, this was not reflected in the documentation. --- docs/using-the-compiler.rst | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index c6c40cacc..067c96c96 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -410,12 +410,13 @@ Input Description "source1.sol": ["contract1"], "source2.sol": ["contract2", "contract3"] }, - // Choose whether division and modulo operations should be replaced by - // multiplication with slack variables. Default is `true`. - // Using `false` here is recommended if you are using the CHC engine + // Choose how division and modulo operations should be encoded. + // When using `false` they are replaced by multiplication with slack + // variables. This is the default. + // Using `true` here is recommended if you are using the CHC engine // and not using Spacer as the Horn solver (using Eldarica, for example). // See the Formal Verification section for a more detailed explanation of this option. - "divModWithSlacks": true, + "divModNoSlacks": false, // Choose which model checker engine to use: all (default), bmc, chc, none. "engine": "chc", // Choose which types of invariants should be reported to the user: contract, reentrancy.