From 0d3ea6f2dcaf80d386c7765ee8a708c18e3ed574 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 16 Mar 2021 12:19:46 -0300 Subject: [proof-new] Renaming proof option to be in sync with SMT-LIB (#6154) --- src/theory/arith/proof_macros.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/arith') diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h index dfb3ddad8..d453285d6 100644 --- a/src/theory/arith/proof_macros.h +++ b/src/theory/arith/proof_macros.h @@ -21,11 +21,11 @@ #include "options/smt_options.h" #define ARITH_PROOF(x) \ - if (CVC4::options::proof()) \ + if (CVC4::options::produceProofs()) \ { \ x; \ } -#define ARITH_NULLPROOF(x) (CVC4::options::proof()) ? x : NULL -#define ARITH_PROOF_ON() CVC4::options::proof() +#define ARITH_NULLPROOF(x) (CVC4::options::produceProofs()) ? x : NULL +#define ARITH_PROOF_ON() CVC4::options::produceProofs() #endif // CVC4__THEORY__ARITH__PROOF_MACROS_H -- cgit v1.2.3