From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 11 Mar 2022 21:09:53 +0000 (-0600)
Subject: Fix maximum value for pedantic proof level (#8246)
X-Git-Tag: cvc5-1.0.0~276
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27d2b3463c0da8e70ccacbb79efb267281ffd670;p=cvc5.git

Fix maximum value for pedantic proof level (#8246)

Fixes cvc5/cvc5-projects#357.
Now gives:
(error "Error in option parsing: proof-pedantic = 5773657586652532005 is not a legal setting, value should be at most 100.")
---

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 346a0dc4e..e6c2386b7 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -39,6 +39,7 @@ name   = "Proof"
   long       = "proof-pedantic=N"
   type       = "uint64_t"
   default    = "0"
+  maximum    = "100"
   help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
 
 [[option]]
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 8da98e399..e8b07a819 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -40,7 +40,7 @@ PfManager::PfManager(Env& env)
     : EnvObj(env),
       d_pchecker(new ProofChecker(
           options().proof.proofCheck == options::ProofCheckMode::EAGER,
-          options().proof.proofPedantic)),
+          static_cast<uint32_t>(options().proof.proofPedantic))),
       d_pnm(new ProofNodeManager(
           env.getOptions(), env.getRewriter(), d_pchecker.get())),
       d_pppg(nullptr),