From d70d137898cb8522a8b2f1e72ea4b6dd4df1e681 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Sun, 15 May 2022 17:45:52 +0200 Subject: [PATCH] Changelog and docs --- Changelog.md | 2 ++ docs/smtchecker.rst | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index 77a804720..62b302860 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,7 +12,9 @@ Compiler Features: * Assembly-Json: Export: Include source list in `sourceList` field. * Commandline Interface: option ``--pretty-json`` works also with the following options: ``--abi``, ``--asm-json``, ``--ast-compact-json``, ``--devdoc``, ``--storage-layout``, ``--userdoc``. * SMTChecker: Support ``abi.encodeCall`` taking into account the called selector. + * SMTChecker: Use the Horn solver Eldarica via its binary if installed in the system. It can be enabled via the CLI option ``--model-checker-solvers eld`` or the JSON field ``settings.modelChecker.solvers=["eld"]``. * SMTChecker: New trusted mode that assumes that any compile-time available code is the actual used code even in external calls. This can be used via the CLI option ``--model-checker-ext-calls=trusted`` or the JSON field ``settings.modelChecker.extCalls: "trusted"``. +>>>>>>> e0e01b952 (Changelog and docs) * Language Server: Allow full filesystem access to language server. diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index 698c96f8f..b6c95d7c7 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -653,10 +653,11 @@ which is primarily an SMT solver and makes `Spacer `_ which does both. The user can choose which solvers should be used, if available, via the CLI -option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option +option ``--model-checker-solvers {all,cvc4,eld,smtlib2,z3}`` or the JSON option ``settings.modelChecker.solvers=[smtlib2,z3]``, where: - ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``. +- ``eld`` is used via its binary which must be installed in the system. Only CHC uses ``eld``. - ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 `_ format. These can be used together with the compiler's `callback mechanism `_ so that any solver binary from the system can be employed to synchronously return the results of the queries to the compiler.