-# this is just a placeholder for later; it doesn't show up in command-line options listings
-common-option unsatCores produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- turn on unsat core generation (NOT YET SUPPORTED)
-common-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ after UNSAT/VALID, machine-check the generated proof
+option dumpProofs --dump-proofs bool :default false :link --proof
+ output proofs after every UNSAT/VALID response
+option dumpInstantiations --dump-instantiations bool :default false
+ output instantiations of quantified formulas after every UNSAT/VALID response
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on unsat core generation
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ output unsat cores after every UNSAT/VALID response
+
+option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"