From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Apr 2021 14:57:36 +0000 (-0500)
Subject: Enable print-inst-full by default (#6435)
X-Git-Tag: cvc5-1.0.0~1833
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4eb2234bccf033e3758a7fb7309f51f4864cba0a;p=cvc5.git

Enable print-inst-full by default (#6435)

This makes dump-instantiations print instantiations for all quantified formulas by default, regardless of whether they had an associated identifier.
---

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index 1f27326a0..d72279f95 100644
--- 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"