projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: bff2975)
Enable print-inst-full by default (#6435)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 26 Apr 2021 14:57:36 +0000 (09:57 -0500)
committerGitHub <noreply@github.com>
Mon, 26 Apr 2021 14:57:36 +0000 (14:57 +0000)
This makes dump-instantiations print instantiations for all quantified formulas by default, regardless of whether they had an associated identifier.

src/options/printer_options.toml patch | blob | history

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index 1f27326a0aa45ebd20372f0e0421e6116d21dac3..d72279f95e067db5bb4fa9dbbe81fc09e57ee376 100644 (file)
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -64,5 +64,5 @@ header = "options/printer_options.h"
   category   = "regular"
   long       = "print-inst-full"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "print instantiations for formulas that do not have given identifiers"