diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 13:04:55 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-15 20:04:55 +0000 |
| commit | 77bca094a140b35341257f125a55212ff0108250 (patch) | |
| tree | 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /src/options/quantifiers_options.toml | |
| parent | 63647b1d79df6f287ea6599958b16fce44b8271d (diff) | |
Rename occurrences of CVC4 to CVC5. (#6351)
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index bbdf030a1..076d26553 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -994,7 +994,7 @@ header = "options/quantifiers_options.h" # Solution reconstruction modes for single invocation conjectures # -# These modes indicate the policy when CVC4 solves a synthesis conjecture using +# These modes indicate the policy when cvc5 solves a synthesis conjecture using # single invocation techniques for a sygus problem with a user-specified # grammar. # @@ -1008,7 +1008,7 @@ header = "options/quantifiers_options.h" help_mode = "Modes for reconstruction solutions while using single invocation techniques." [[option.mode.NONE]] name = "none" - help = "Do not try to reconstruct solutions in the original (user-provided) grammar when using single invocation techniques. In this mode, solutions produced by CVC4 may violate grammar restrictions." + help = "Do not try to reconstruct solutions in the original (user-provided) grammar when using single invocation techniques. In this mode, solutions produced by cvc5 may violate grammar restrictions." [[option.mode.TRY]] name = "try" help = "Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner." @@ -1538,7 +1538,7 @@ header = "options/quantifiers_options.h" long = "sygus-query-gen-check" type = "bool" default = "true" - help = "use interesting satisfiability queries to check soundness of CVC4" + help = "use interesting satisfiability queries to check soundness of cvc5" [[option]] name = "sygusQueryGenDumpFiles" |