1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
Description: fix typos
Author: J.Puydt
Forwarded: yes
--- cryptominisat.orig/scripts/check_lpn_solution.py
+++ cryptominisat/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)
--- cryptominisat.orig/scripts/translate_opb.py
+++ cryptominisat/scripts/translate_opb.py
@@ -103,7 +103,7 @@
c.lhs[i][0] = -c.lhs[i][0]
leq_translate(c)
else:
- print("ERRROR")
+ print("ERROR")
exit(-1)
--- cryptominisat.orig/src/get_clause_query.cpp
+++ cryptominisat/src/get_clause_query.cpp
@@ -73,7 +73,7 @@
if (simplified) {
bva_vars = true;
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);
--- cryptominisat.orig/src/occsimplifier.cpp
+++ cryptominisat/src/occsimplifier.cpp
@@ -5527,7 +5527,7 @@
if (cl->freed() || cl->getRemoved()) 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);
}
}
--- cryptominisat.orig/src/picosat/picosat.c
+++ cryptominisat/src/picosat/picosat.c
@@ -7472,7 +7472,7 @@
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 @@
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]);
}
}
--- cryptominisat.orig/src/solver.cpp
+++ cryptominisat/src/solver.cpp
@@ -1632,7 +1632,7 @@
case -2: cout << "ERROR reported by tbuddy: VAR (-2) /* Unknown variable */" << endl; break;
case -3: cout << "ERROR reported by tbuddy: RANGE (-3) /* Variable value out of range (not in domain) */" << endl; break;
case -4: cout << "ERROR reported by tbuddy: DEREF (-4) /* Removing external reference to unknown node */" << endl; break;
- case -5: cout << "ERROR reported by tbuddy: RUNNING (-5) /* Called bdd_init() twice whithout bdd_done() */" << endl; break;
+ case -5: cout << "ERROR reported by tbuddy: RUNNING (-5) /* Called bdd_init() twice without bdd_done() */" << endl; break;
case -6: cout << "ERROR reported by tbuddy: FILE (-6) /* Some file operation failed */" << endl; break;
case -7: cout << "ERROR reported by tbuddy: FORMAT (-7) /* Incorrect file format */" << endl; break;
case -8: cout << "ERROR reported by tbuddy: ORDER (-8) /* Vars. not in order for vector based functions */" << endl; break;
|
