mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Fix some typos in identifiers. (#7118)

Browse source
This commit is contained in:
Bruce Mitchener 2024-02-14 09:25:32 +07:00 • committed by GitHub
parent dba2f788df
commit 155dfb10c4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/z3_api.h
View file

@ -1363,7 +1363,7 @@ typedef enum {
- Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file. - Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
- Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier. - Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
- Z3_MEMOUT_FAIL: A memory allocation failure was encountered. - Z3_MEMOUT_FAIL: A memory allocation failure was encountered.
- Z3_FILE_ACCESS_ERRROR: A file could not be accessed. - Z3_FILE_ACCESS_ERROR: A file could not be accessed.
- Z3_INVALID_USAGE: API call is invalid in the current state. - Z3_INVALID_USAGE: API call is invalid in the current state.
- Z3_INTERNAL_FATAL: An error internal to Z3 occurred. - Z3_INTERNAL_FATAL: An error internal to Z3 occurred.
- Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with #Z3_inc_ref. - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with #Z3_inc_ref.

4
src/smt/theory_arith_int.h
View file

@ -99,7 +99,7 @@ namespace smt {
theory_var result = null_theory_var; theory_var result = null_theory_var;
numeral range; numeral range;
numeral new_range; numeral new_range;
numeral small_range_thresold(1024); numeral small_range_threshold(1024);
unsigned n = 0; unsigned n = 0;
for (row const& row : m_rows) { for (row const& row : m_rows) {
theory_var v = row.get_base_var(); theory_var v = row.get_base_var();
@ -117,7 +117,7 @@ namespace smt {
numeral const & u = upper_bound(v).get_rational(); numeral const & u = upper_bound(v).get_rational();
new_range = u; new_range = u;
new_range -= l; new_range -= l;
if (new_range > small_range_thresold) { if (new_range > small_range_threshold) {
// //
} }
else if (result == null_theory_var || new_range < range) { else if (result == null_theory_var || new_range < range) {

6
src/util/sexpr.cpp
View file

@ -26,11 +26,11 @@ Notes:
#endif #endif
struct sexpr_composite : public sexpr { struct sexpr_composite : public sexpr {
unsigned m_num_chilren; unsigned m_num_children;
sexpr * m_children[0]; sexpr * m_children[0];
sexpr_composite(unsigned num_children, sexpr * const * children, unsigned line, unsigned pos): sexpr_composite(unsigned num_children, sexpr * const * children, unsigned line, unsigned pos):
sexpr(kind_t::COMPOSITE, line, pos), sexpr(kind_t::COMPOSITE, line, pos),
m_num_chilren(num_children) { m_num_children(num_children) {
for (unsigned i = 0; i < num_children; i++) { for (unsigned i = 0; i < num_children; i++) {
m_children[i] = children[i]; m_children[i] = children[i];
children[i]->inc_ref(); children[i]->inc_ref();
@ -107,7 +107,7 @@ std::string const & sexpr::get_string() const {
unsigned sexpr::get_num_children() const { unsigned sexpr::get_num_children() const {
SASSERT(is_composite()); SASSERT(is_composite());
return static_cast<sexpr_composite const *>(this)->m_num_chilren; return static_cast<sexpr_composite const *>(this)->m_num_children;
} }
sexpr * sexpr::get_child(unsigned idx) const { sexpr * sexpr::get_child(unsigned idx) const {