diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5947367f2..151b6106b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -269,7 +269,7 @@ class CVC4_EXPORT SmtEngine * block-models option is set to a mode other than "none". * * This adds an assertion to the assertion stack that blocks the current - * model based on the current options configured by CVC4. + * model based on the current options configured by cvc5. * * The return value has the same meaning as that of assertFormula. */ @@ -704,14 +704,14 @@ class CVC4_EXPORT SmtEngine /** * Get an unsatisfiable core (only if immediately preceded by an UNSAT or - * ENTAILED query). Only permitted if CVC4 was built with unsat-core support + * ENTAILED query). Only permitted if cvc5 was built with unsat-core support * and produce-unsat-cores is on. */ UnsatCore getUnsatCore(); /** * Get a refutation proof (only if immediately preceded by an UNSAT or - * ENTAILED query). Only permitted if CVC4 was built with proof support and + * ENTAILED query). Only permitted if cvc5 was built with proof support and * the proof option is on. */ std::string getProof(); @@ -750,9 +750,9 @@ class CVC4_EXPORT SmtEngine * limit, but it's deterministic so that reproducible results can be * obtained. Currently, it's based on the number of conflicts. * However, please note that the definition may change between different - * versions of CVC4 (as may the number of conflicts required, anyway), + * versions of cvc5 (as may the number of conflicts required, anyway), * and it might even be different between instances of the same version - * of CVC4 on different platforms. + * of cvc5 on different platforms. * * A cumulative and non-cumulative (per-call) resource limit can be * set at the same time. A call to setResourceLimit() with @@ -927,7 +927,7 @@ class CVC4_EXPORT SmtEngine /** * Internal method to get an unsatisfiable core (only if immediately preceded - * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with + * by an UNSAT or ENTAILED query). Only permitted if cvc5 was built with * unsat-core support and produce-unsat-cores is on. Does not dump the * command. */ @@ -983,7 +983,7 @@ class CVC4_EXPORT SmtEngine * return nullptr. * * This ensures that the underlying theory model of the SmtSolver maintained - * by this class is currently available, which means that CVC4 is producing + * by this class is currently available, which means that cvc5 is producing * models, and is in "SAT mode", otherwise a recoverable exception is thrown. * * @param c used for giving an error message to indicate the context |