diff --git a/scripts/check_lpn_solution.py b/scripts/check_lpn_solution.py index bf022d3b9..575e4ab13 100755 --- a/scripts/check_lpn_solution.py +++ b/scripts/check_lpn_solution.py @@ -54,7 +54,7 @@ sol[var] = lit > 0 if sat is None: - print("ERRROR could not recover solution from SAT output") + print("ERROR could not recover solution from SAT output") exit(-1) # print("Recovered SAT: ", sat) diff --git a/scripts/translate_opb.py b/scripts/translate_opb.py index 57b15fe64..4b878d5e1 100755 --- a/scripts/translate_opb.py +++ b/scripts/translate_opb.py @@ -103,7 +103,7 @@ def translate(self): c.lhs[i][0] = -c.lhs[i][0] leq_translate(c) else: - print("ERRROR") + print("ERROR") exit(-1) diff --git a/src/get_clause_query.cpp b/src/get_clause_query.cpp index 2ae1dff0f..7e132a589 100644 --- a/src/get_clause_query.cpp +++ b/src/get_clause_query.cpp @@ -62,7 +62,7 @@ void GetClauseQuery::start_getting_constraints(bool _red, bool _simplified, simplified = _simplified; if (simplified) { if (solver->get_num_bva_vars() != 0) { - cout << "ERRROR! You must not have BVA variables for simplified CNF getting" << endl; + cout << "ERROR! You must not have BVA variables for simplified CNF getting" << endl; exit(-1); } release_assert(solver->get_num_bva_vars() == 0); diff --git a/src/mpicosat/mpicosat.c b/src/mpicosat/mpicosat.c index c32638630..bcd61c99b 100644 --- a/src/mpicosat/mpicosat.c +++ b/src/mpicosat/mpicosat.c @@ -7472,7 +7472,7 @@ picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fi assert (res == 20); if (ps->verbosity > 1) fprintf (ps->out, - "%ssuceeded to drop %d%s assumption %d\n", + "%ssucceeded to drop %d%s assumption %d\n", ps->prefix, i, enumstr (i), work[i]); redundant[i] = 1; for (j = 0; j < nwork; j++) @@ -7489,7 +7489,7 @@ picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fi redundant[j] = -1; if (ps->verbosity > 1) fprintf (ps->out, - "%salso suceeded to drop %d%s assumption %d\n", + "%salso succeeded to drop %d%s assumption %d\n", ps->prefix, j, enumstr (j), work[j]); } } diff --git a/src/occsimplifier.cpp b/src/occsimplifier.cpp index 3a8d2f338..cda3d94a1 100644 --- a/src/occsimplifier.cpp +++ b/src/occsimplifier.cpp @@ -5429,7 +5429,7 @@ void OccSimplifier::check_clauses_lits_ordered() const if (cl->freed() || cl->get_removed()) continue; for(uint32_t i = 1; i < cl->size(); i++) { if ((*cl)[i-1] >= (*cl)[i]) { - cout << "ERRROR cl: " << *cl << endl; + cout << "ERROR cl: " << *cl << endl; assert(false); } }