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 346a0dc4e159a316503f665d578fe67720fe1be4..e6c2386b7f9ee28861a826184b2255ea045e98ce 100644 (file)
--- 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 8da98e399bf015bde80f27ec37e1405f42e62e0f..e8b07a819d4f88411b2f96849e5d9bd8a22c3bde 100644 (file)
--- 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),