From f69b2744aed5c08e5b717e8c668f5463fb8f0fcd Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Wed, 23 Nov 2022 08:10:01 +0100 Subject: [PATCH] README: Update --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index e98c3c95..9cb4b66c 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Golem can be compiled on Linux and MacOS. It uses `CMake` for build configuration. Golem depends on [OpenSMT](https://github.com/usi-verification-and-security/opensmt/) for SMT solving and interpolation. If you already have OpenSMT installed, you can pass the path using `-DOPENSMT_HOME` option to `cmake` command. -Note that Golem requires a specific version of OpenSMT, currently v2.4.2. +Note that Golem requires a specific version of OpenSMT, currently v2.4.3. Otherwise, `cmake` will download the latest compatible version of OpenSMT and build it as a subproject. ## Usage @@ -22,8 +22,8 @@ You can view the usage in the help message after running $ golem -h ``` -At the moment, you must specified the SMT theory used in the CHC encoding with `-l` option. The supported theories are `QF_LRA` and `QF_LIA`, i.e., the linear arithmetic over reals or integers. -We plan to remove this requirement and automatically detect the theory in the future. +At the moment, you should specified the SMT theory used in the CHC encoding with `-l` option. The supported theories are `QF_LRA` and `QF_LIA`, i.e., the linear arithmetic over reals or integers. +Golem now has limited support to automatically detect the theory from the script, so the option is no longer mandatory, but still recommended. ### Backend engines Golem currently supports 5 different backend algorithms for solving CHCs.