From 27d2b3463c0da8e70ccacbb79efb267281ffd670 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Mar 2022 15:09:53 -0600 Subject: [PATCH] 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.") --- src/options/proof_options.toml | 1 + src/smt/proof_manager.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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(options().proof.proofPedantic))), d_pnm(new ProofNodeManager( env.getOptions(), env.getRewriter(), d_pchecker.get())), d_pppg(nullptr), -- 2.30.2