Fix spelling errors

src/ast/dl_decl_plugin.cpp

@@ -461,7 +461,7 @@ namespace datalog {
             return 0;
         }
         if (!ps.is_ast() || !is_sort(ps.get_ast()) || !is_fin_sort(to_sort(ps.get_ast()))) {
-            m_manager->raise_exception("second paramter should be a finite domain sort");
+            m_manager->raise_exception("second parameter should be a finite domain sort");
             return 0;
         }
         sort* s = to_sort(ps.get_ast());

src/ast/normal_forms/pull_quant.cpp

@@ -125,8 +125,8 @@ struct pull_quant::imp {
                         //   of nested_q->get_expr().
                         m_shift(nested_q->get_expr(), 
                                 nested_q->get_num_decls(),             // bound for shift1/shift2
-                                num_decls - nested_q->get_num_decls(), // shift1  (shift by this ammount if var idx >= bound)
+                                num_decls - nested_q->get_num_decls(), // shift1  (shift by this amount if var idx >= bound)
-                                shift_amount,                          // shift2  (shift by this ammount if var idx < bound)
+                                shift_amount,                          // shift2  (shift by this amount if var idx < bound)
                                 adjusted_child);
                         TRACE("pull_quant", tout << "shifted  bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount <<
                               " shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) << 

src/ast/pp_params.pyg

@@ -15,5 +15,5 @@ def_module_params('pp',
                           ('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'),
                           ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),
                           ('single_line', BOOL, False, 'ignore line breaks when true'),
-                          ('bounded', BOOL, False, 'ignore characters exceeding max widht'),
+                          ('bounded', BOOL, False, 'ignore characters exceeding max width'),
                           ('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing')))

src/cmd_context/cmd_util.cpp

@@ -6,7 +6,7 @@ Module Name:
     cmd_util.cpp
 
 Abstract:
-    Macros for definining new SMT2 front-end cmds.
+    Macros for defining new SMT2 front-end cmds.
 
 Author:
 

src/cmd_context/cmd_util.h

@@ -6,7 +6,7 @@ Module Name:
     cmd_util.h
 
 Abstract:
-    Macros for definining new SMT2 front-end cmds.
+    Macros for defining new SMT2 front-end cmds.
 
 Author:
 

src/cmd_context/tactic_cmds.cpp

@@ -97,7 +97,7 @@ void help_tactic(cmd_context & ctx) {
     buf << "- (or-else <tactic>+) tries the given tactics in sequence until one of them succeeds (i.e., the first that doesn't fail).\n";
     buf << "- (par-or <tactic>+) executes the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).\n";
     buf << "- (par-then <tactic1> <tactic2>) executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.\n";
-    buf << "- (try-for <tactic> <num>) excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds.\n";
+    buf << "- (try-for <tactic> <num>) executes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds.\n";
     buf << "- (if <probe> <tactic> <tactic>) if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second.\n";
     buf << "- (when <probe> <tactic>) shorthand for (if <probe> <tactic> skip).\n";
     buf << "- (fail-if <probe>) fail if <probe> evaluates to true.\n";

src/math/subpaving/subpaving_t.h

@@ -354,7 +354,7 @@ public:
     };
 
     /**
-       \brief Watched element (aka occurence) can be:
+       \brief Watched element (aka occurrence) can be:
        
        - A clause
        - A definition (i.e., a variable)

src/muz/base/dl_util.h

@@ -591,7 +591,7 @@ namespace datalog {
 
 
     /**
-       \brief Remove the first occurence of \c el from \c v and return \c true. If
+       \brief Remove the first occurrence of \c el from \c v and return \c true. If
        \c el is not present in \c v, return \c false. The order of elements in \c v
        is not preserved.
      */

src/muz/fp/datalog_parser.cpp

@@ -480,7 +480,7 @@ protected:
     str2sort          m_sort_dict;
 
     
-    // true if an error occured during the current call to the parse_stream
+    // true if an error occurred during the current call to the parse_stream
     // function
     bool              m_error;
 public:
@@ -896,7 +896,7 @@ protected:
                 tok = m_lexer->next_token();
                 if (tok != TK_COLON) {
                     tok = unexpected(tok, 
-                        "Expecting colon in declaration (first occurence of a predicate must be a declaration)");
+                        "Expecting colon in declaration (first occurrence of a predicate must be a declaration)");
                     return tok;
                 }
                 tok = m_lexer->next_token();

src/smt/params/smt_params_helper.pyg

@@ -13,7 +13,7 @@ def_module_params(module_name='smt',
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
                           ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
-                          ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
+                          ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (0 means immediate timeout)'),

src/smt/smt_context_pp.cpp

@@ -253,7 +253,7 @@ namespace smt {
 
     void context::display_app_enode_map(std::ostream & out) const {
         if (!m_e_internalized_stack.empty()) {
-            out << "expresion -> enode:\n";
+            out << "expression -> enode:\n";
             unsigned sz = m_e_internalized_stack.size();
             for (unsigned i = 0; i < sz; i++) {
                 expr *  n = m_e_internalized_stack.get(i);
@@ -265,7 +265,7 @@ namespace smt {
 
     void context::display_expr_bool_var_map(std::ostream & out) const {
         if (!m_b_internalized_stack.empty()) {
-            out << "expresion -> bool_var:\n";
+            out << "expression -> bool_var:\n";
             unsigned sz = m_b_internalized_stack.size();
             for (unsigned i = 0; i < sz; i++) {
                 expr *  n  = m_b_internalized_stack.get(i);

src/tactic/arith/diff_neq_tactic.h

@@ -29,6 +29,6 @@ class tactic;
 
 tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p = params_ref());
 /*
-  ADD_TACTIC("diff-neq", "specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numberal, and all constants are bounded.", "mk_diff_neq_tactic(m, p)")
+  ADD_TACTIC("diff-neq", "specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numeral, and all constants are bounded.", "mk_diff_neq_tactic(m, p)")
 */
 #endif

src/tactic/probe.h

@@ -62,7 +62,7 @@ probe * mk_depth_probe();
 probe * mk_size_probe();
 
 /*
-  ADD_PROBE("memory", "ammount of used memory in megabytes.", "mk_memory_probe()")
+  ADD_PROBE("memory", "amount of used memory in megabytes.", "mk_memory_probe()")
   ADD_PROBE("depth", "depth of the input goal.", "mk_depth_probe()")
   ADD_PROBE("size", "number of assertions in the given goal.", "mk_size_probe()")
 */

src/tactic/sls/sls_tracker.h

@@ -464,7 +464,7 @@ public:
             if (!m_weights.contains(e))
         		m_weights.insert(e, m_paws_init);
 
-            // positive/negative occurences used for early pruning
+            // positive/negative occurrences used for early pruning
             setup_occs(as[i]);
         }
 

src/util/mpff.h

@@ -94,7 +94,7 @@ class mpff_manager {
     //
     // - All values of type int, unsigned, int64 and uint64 can be precisely represented as mpff numerals.
     //
-    // - Hardware float and double values (corresponding to rationals) can also be precisely represented as mpff numberals.
+    // - Hardware float and double values (corresponding to rationals) can also be precisely represented as mpff numerals.
     //   That is, NaN, +oo and -oo are not supported by this module.
     //
     // - An exception (mpff_manager::exception) is thrown if overflow occurs. This can happen because the exponent is