[Arch-excludes] Architecture specific change in rpms/cryptominisat4.git

The package rpms/cryptominisat4.git has added or updated architecture specific content in
its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/cryptominisat4.git/commit/?id=a94....

Change:
-%ifnarch s390

Thanks.


Full change:
============

commit a945b4b48e6f376b4f62e8066138df3289b08059
Author: Jerry James <loganjerry(a)gmail.com&gt;
Date:   Sun Jul 22 20:58:56 2018 -0600

    Obsoleted by cryptominisat (version 5.x)

diff --git a/.gitignore b/.gitignore
deleted file mode 100644
index 6f02586..0000000
--- a/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/4.5.3.tar.gz
diff --git a/cryptominisat4-heap.patch b/cryptominisat4-heap.patch
deleted file mode 100644
index 3d9cffc..0000000
--- a/cryptominisat4-heap.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/heap.h.orig	2015-08-26 17:32:30.000000000 -0600
-+++ src/heap.h	2018-02-13 20:27:38.953218262 -0700
-@@ -108,7 +108,7 @@ class Heap {
-         return heap[at+1];
-     }
- 
--    void operator=(const Heap<Comp>& other)
-+    Heap<Comp>& operator=(const Heap<Comp>& other)
-     {
-         heap.resize(other.heap.size());
-         std::copy(other.heap.begin(), other.heap.end(), heap.begin());
diff --git a/cryptominisat4.1 b/cryptominisat4.1
deleted file mode 100644
index af0ece8..0000000
--- a/cryptominisat4.1
+++ /dev/null
@@ -1,504 +0,0 @@
-.TH "CRYPTOMINISAT" "1" "@VERSION@" "Mate Soos"
"User Commands"
-.SH "NAME"
-cryptominisat \- conflict-driven SAT solver
-.SH "SYNOPSIS"
-.B cryptominisat
-[\fIOPTIONS\fP] <\fIinput\-files\fP>
-.SH "DESCRIPTION"
-.PP
-CryptoMiniSat is a SAT solver, solving problems given in CNF, or conjunctive
-normal form. CryptoMiniSat retains much of the API of MiniSat, but
-offers more versatility and better speed on many problems.
-
-The program is a classical conflict-driven solver, with variable activities,
-clause learning and clause deletion. It however incorporates a number of
-advanced CNF simplification functionalities which should help the speed of
-solving. Further, it incorporates some advanced memory-management features
-that should help in getting the most out of modern CPU caches.
-
-The input format is that of DIMACS CNF, i.e. a header of the form
-
-p cnf VARS CLAUSES
-
-where VARS is the number of variables, and CLAUSES is the number of clauses in
-the problem. It then lists the set of clauses such as:
-
-1 -2 0
-
-which is equivalent to the 2-long clause "v1 OR NOT v2 = TRUE"
-
-.SH "OPTIONS"
-.TP
-\fB\-h,\-\-help\fP
-Print help text.
-.TP
-\fB\-v,\-\-version\fP
-Print cryptominisat's version number.
-.TP
-\fB\-\-input\fP = <\fIfile1\fP,\fIfile2\fP,...>
-Specify the file(s) to read.
-.TP
-\fB\-r,\-\-random\fP = <\fIseed\fP> [0 - 2^32-1]
-Sets the random seed, used for picking decision variables (default = 0).
-.TP
-\fB\-t,\-\-threads\fP = <\fInum\fP> [1..]
-Number of threads (default is 1).
-.TP
-\fB\-\-sync\fP = <\fInum\fP>
-Sync threads every \fInum\fP conflicts (default = 6000).
-.TP
-\fB\-\-maxtime\fP = <\fInum\fP>
-Stop solving after this much time, print stats and exit.
-.TP
-\fB\-\-maxconfl\fP = <\fInum\fP>
-Stop solving after this many conflicts, print stats and exit.
-.TP
-\fB\-\-occsimp\fP = \fI{0,1}\fP
-Perform occurrence-list-based optimizations, such as variable eliminiation,
-subsumption, and bounded variable addition.  Default is 1.
-.TP
-\fB\-\-clbtwsimp\fP = <\fInum\fP>
-Perform this many cleaning iterations between simplification rounds
-(default = 2).
-.TP
-\fB\-d,\-\-drup\fP = \fI{0,1}\fP
-Put DRUP verification information into this file.
-.TP
-\fB\-\-drupexistscheck\fP = \fI{0,1}\fP
-Check if the DRUP file provided already exists (default = 1).
-.TP
-\fB\-\-drupdebug\fP = \fI{0,1}\fP
-Output DRUP verification to the console.  This is helpful to see where DRUP
-fails.  Use in conjunction with \fB--verb 20\fP.
-.SS "RESTART"
-.TP
-\fB\-\-agilg\fP = <\fInum\fP>
-See paper by Armin Biere on agilities.
-.TP
-\fB\-\-restart\fP = \fI{geom,agility,glue,glueagility}\fP
-Choose the restart strategy to follow.
-.TP
-\fB\-\-agillim\fP = <\fInum\fP>
-The agility below which the agility is considered too low (default = 0.03).
-.TP
-\fB\-\-agilviollim\fP = <\fInum\fP>
-The number of agility violations over which to demand a restart (default = 20).
-.TP
-\fB\-\-gluehist\fP = <\fInum\fP>
-The size of the moving window for short term glue history of redundant
-clauses (default = 100).  If higher, the minimal number of conflicts between
-restarts is longer.
-.TP
-\fB\-\-blkrest\fP = \fI{0,1}\fP
-Perform blocking restarts as per Glucose 3.0 (default = 1).
-.TP
-\fB\-\-blkrestlen\fP = <\fInum\fP>
-The length of the long term trail size for blocking restart (default = 5000).
-.TP
-\fB\-\-blkrestmultip\fP = <\fInum\fP>
-Multiplier used for blocking restart cut-off, called "R" in Glucose 3.0
-(default = 1.4).
-.SS "PRINTING"
-.TP
-\fB\-\-verb\fP = <\fInum\fP> [0-10]
-Verbosity of the solver (default = 2).  Verbosity 0 only prints the results.
-.TP
-\fB\-\-verbstat\fP = \fI{0,1}\fP
-Turns off verbose stats if needed (default = 1).
-.TP
-\fB\-\-printfull\fP = \fI{0,1}\fP
-Print more thorough, but different, stats (default = 0).
-.TP
-\fB\-s,\-\-printsol\fP = \fI{0,1}\fP
-Print the satisfying assignment if the solution is SAT (default = 1).
-.TP
-\fB\-\-printtrail\fP = <\fInum\fP>
-Print the longest decision trail of the last N conflicts; if 0, the decision
-trail is not printed (default = 0).
-.TP
-\fB\-\-printbest\fP = <\fInum\fP>
-Print the best N irredundant longer-than-3 learnt clauses; if 0, nothing is
-printed (default = 0).
-.TP
-\fB\-\-printtimes\fP = \fI{0,1}\fP
-Print the time taken for each simplification run; if 0, nothing is printed,
-which makes logs easier to compare (default = 1).
-.SS "PROPAGATION"
-.TP
-\fB\-\-updateglue\fP = \fI{0,1}\fP
-Update glues while propagating (default = 1).
-.TP
-\fB\-\-lhbr\fP = \fI{0,1}\fP
-Perform lazy hyper-binary resolution while propagating (default = 0).
-.TP
-\fB\-\-binpri\fP = \fI{0,1}\fP
-Propagated binary clauses are strictly first (default = 0).
-.TP
-\fB\-\-otfhyper\fP = \fI{0,1}\fP
-Perform hyper-binary resolution at decision level 1 after every restart and
-during probing (default = 1).
-.SS "REDUNDANT CLAUSE REMOVAL"
-.TP
-\fB\-\-ltclean\fP = <\fInum\fP> [0-1]
-Remove at least this ratio of redundant clauses when doing redundant clause
-cleaning (default = 0.5).
-.TP
-\fB\-\-clean\fP = \fI{size,glue,activity,prconf,confdep}\fP
-Metric used to clean clauses (default = prconf).  Use "prconf" for the sum of
-propagations and conflicts.  Use "confdep" for (propagations + conflicts) /
-(depth at which they were caused).
-.TP
-\fB\-\-noremfreshgl2\fP = \fI{0,1}\fP
-Don't remove glue 2 clauses that are fresh (default = 0).
-.TP
-\fB\-\-cleanconflmult\fP = <\fInum\fP>
-If propagations and conflicts are used to clean, the value by which conflicts
-are multiplied relative to propagations (default = 1).  Conflicts are much
-rarer, but maybe more useful.
-.TP
-\fB\-\-lockuip\fP = <\fInum\fP>
-The number of clauses to lock into the database per cleaning based on UIP usage
-(default = 500).
-.TP
-\fB\-\-locktop\fP = <\fInum\fP>
-The number of clauses to lock into the database per cleaning based on the best
-uncleaned clauses as per the selected heuristic (default = 0).
-.TP
-\fB\-\-perfmult\fP = <\fInum\fP>
-Value by which to multiply clause performance values after every clause cleaning
-(default = 0).
-.TP
-\fB\-\-clearstat\fP = \fI{0,1}\fP
-Clear clause statistics data of each clause after clause cleaning (default = 1).
-.TP
-\fB\-\-startclean\fP = <\fInum\fP>
-Clean the first time after this many conflicts (default = 10000).
-.TP
-\fB\-\-incclean\fP = <\fInum\fP>
-Clean increment cleaning by this factor for the next cleaning (default = 1.1).
-.TP
-\fB\-\-maxredratio\fP = <\fInum\fP>
-Never have more than N * (irred_clauses) redundant clauses (default = 10).
-.SS "VARIABLE BRANCHING"
-.TP
-\fB\-\-vincmult\fP = <\fInum\fP>
-Variable activity increase multipler (default = 11).
-.TP
-\fB\-\-vincdiv\fP = <\fInum\fP>
-Variable activity increase divider (default = 10); it \fBmust\fP be smaller
-than the multiplier.
-.TP
-\fB\-\-vincvary\fP = <\fInum\fP>
-Variable activity divider and multiplier are both changed +/- this amount,
-randomly, in sync (default = 0).
-.TP
-\fB\-\-vincstart\fP = <\fInum\fP>
-Variable activity increase stars with this value.  Make sure that this,
-multiplied by the multiplier and divided by the divider, is larger than itself
-(default = 128).
-.TP
-\fB\-\-freq\fP = <\fInum\fP> [0-1]
-Frequency of picking decision variables at random (default = 0).
-.TP
-\fB\-\-dompickf\fP = <\fInum\fP>
-Use the dominating literal once in every N when picking decision literal
-(default = 400).
-.TP
-\fB\-\-morebump\fP = \fI{0,1}\fP
-Bump variables' activities based on the glue of redundant clauses there are in
-during UIP generation, as per Glucose (default = 1).
-.SS "VARIABLE POLARITY"
-.TP
-\fB\-\-polar\fP = \fI{true,false,rnd,auto}\fP
-Selects the polarity mode (default = auto).  True selects only positive
-polarity when branching.  False selects only negative polarity when branching.
-Auto selects the last polarity used (also called 'caching').
-.TP
-\fB\-\-calcpolar1st\fP = \fI{0,1}\fP
-Calculate the polarity of variables based on their occurrences at startup of
-solve() (default = 1).
-.TP
-\fB\-\-calcpolarall\fP = \fI{0,1}\fP
-Calculate the polarity of variables based on their occurrences at startup and
-after every simplification (default = 1).
-.SS "CONFLICT"
-.TP
-\fB\-\-recur\fP = \fI{0,1}\fP
-Perform recursive minimisation.
-.TP
-\fB\-\-moreminim\fP = \fI{0,1}\fP
-Perform strong minimisation at conflict gen.
-.TP
-\fB\-\-moreminimcache\fP = <\fInum\fP>
-Timeout in microsteps for each more minimisation with cache (default = 200).
-Only active if 'moreminim' is on.
-.TP
-\fB\-\-moreminimbin\fP = <\fInum\fP>
-Timeout in microsteps for each more minimisation with binary clauses
-(default = 100).  Only active if 'moreminim' is on.
-.TP
-\fB\-\-alwaysmoremin\fP = \fI{0,1}\fP
-Always strong-minimise clauses.
-.TP
-\fB\-\-otfsubsume\fP = \fI{0,1}\fP
-Perform on-the-fly subsumption.
-.TP
-\fB\-\-rewardotfsubsume\fP = <\fInum\fP>
-Reward with this many propagations and conflicts a clause that has been
-shortened with on-the-fly subsumption (default = 3).
-.TP
-\fB\-\-printimpldot\fP = \fI{0,1}\fP
-Print implication graph DOT files, for input into graphviz.
-.SS "ITERATIVE SOLVE"
-.TP
-\fB\-\-maxsol\fP = <\fInum\fP>
-Search for the given number of solutions (default = 1).
-.TP
-\fB\-\-dumpred\fP = <\fIfilename\fP>
-If stopped, dump redundant clauses here.
-.TP
-\fB\-\-maxdump\fP = <\fInum\fP>
-Maximum length of redundant clauses to dump.
-.TP
-\fB\-\-dumpirred\fP = <\fIfilename\fP>
-If stopped, dump irredundant original problems here.
-.TP
-\fB\-\-debuglib\fP
-Solve at specific \fBc Solver::solve()\fP points in the CNF file.  Used to
-debug file generated by Solver's \fBneedLibraryCNFFile()\fP function.
-.TP
-\fB\-\-dumpresult\fP = <\fIfilename\fP>
-Write result(s) to this file.
-.SS "PROBING"
-.TP
-\fB\-\-bothprop\fP = \fI{0,1}\fP
-Do propagations solely to propagate the same value twice (default = 1).
-.TP
-\fB\-\-probe\fP = \fI{0,1}\fP
-Carry out probing (default = 1).
-.TP
-\fB\-\-probemaxm\fP = <\fInum\fP>
-Time in mega-bogoprops to perform probing (default = 1900).
-.TP
-\fB\-\-transred\fP = \fI{0,1}\fP
-Remove useless binary clauses; i.e., transitive reduction (default = 1).
-.SS "STAMPING"
-.TP
-\fB\-\-stamp\fP = \fI{0,1}\fP
-Use time stamping as per the Heule, Javisalo, and Biere paper (default = 1).
-.TP
-\fB\-\-cache\fP = \fI{0,1}\fP
-Use an implication cache (default = 1).  This option may use a lot of memory.
-.TP
-\fB\-\-cachesize\fP = <\fInum\fP>
-Maximum size of the implication cache in MB (default = 2048).  The cache may
-temporarily use more memory, but will be deleted and disabled if this limit is
-reached.
-.TP
-\fB\-\-calcreach\fP = \fI{0,1}\fP
-Calculate literal reachability (default = 1).
-.TP
-\fB\-\-cachecutoff\fP = <\fInum\fP>
-If the number of literals propagated by a literal is greater than this value,
-the literal is not included in the implication cache (default = 2000).
-.SS "SIMPLIFICATION"
-.TP
-\fB\-\-schedsimp\fP = \fI{0,1}\fP
-Perform regular simplification rounds (default = 1).
-.TP
-\fB\-\-presimp\fP = \fI{0,1}\fP
-Perform simplification at the very start (default = 0).
-.TP
-\fB\-\-varelim\fP = \fI{0,1}\fP
-Perform variable elimination as per Een and Biere (default = 1).
-.TP
-\fB\-\-emptyelim\fP = \fI{0,1}\fP
-Perform empty resolvent elimination using the bit-map trick (default = 1).
-.TP
-\fB\-\-elimstrgy\fP = \fI{heuristic,calculate}\fP
-The strategy used to sort variable elimination order (default = heuristic).
-The heuristic strategy uses intelligent guessing.  The calculate strategy uses
-exact calculation.
-.TP
-\fB\-\-elimcplxupd\fP = \fI{0,1}\fP
-Update estimated elimination complexity on-the-fly while eliminating
-(default = 1).
-.TP
-\fB\-\-elimcoststrategy\fP = <\fInum\fP> [0-1]
-How the simple guessing strategy is calculated.
-.TP
-\fB\-\-strengthen\fP = \fI{0,1}\fP
-Perform clause contraction through resolution (default = 1).
-.TP
-\fB\-\-bva\fP = \fI{0,1}\fP
-Perform bounded variable addition (default = 1).
-.TP
-\fB\-\-bvalim\fP = <\fInum\fP>
-Maximum number of variables to add by bounded variable addition per call
-(default = 150000).
-.TP
-\fB\-\-bva2lit\fP = \fI{0,1}\fP
-Bounded variable addition with 2-literal difference hack, too (default = 1).
-Beware, this reduces the effectiveness of 1-literal difference.
-.TP
-\fB\-\-noextbinsubs\fP = \fI{0,1}\fP
-No extended subsumption with binary clauses (default = 1).
-.TP
-\fB\-\-eratio\fP = <\fInum\fP> [0-1]
-Eliminate this ratio of free variables at most per variable elimination
-iteration (default = 0.12).
-.TP
-\fB\-\-skipresol\fP = \fI{0,1}\fP
-Skip BVE resolvents in case they belong to a gate (default = 0).
-.TP
-\fB\-\-occredmax\fP = <\fInum\fP>
-Don't add any redundant clauses larger than this to the occur list
-(default = 200).
-.TP
-\fB\-\-occirredmaxmb\fP = <\fInum\fP>
-Don't allow the irredundant occur size to be more than this many MB
-(default = 800).
-.TP
-\fB\-\-occredmaxmb\fP = <\fInum\fP>
-Don't allow the redundant occur size to be more than this many MB
-(default = 800).
-.SS "EQUIVALENT LITERAL"
-.TP
-\fB\-\-scc\fP = \fI{0,1}\fP
-Find equivalent literals through SCC and replace them (default = 1).
-.TP
-\fB\-\-extscc\fP = \fI{0,1}\fP
-Perform SCC using cache (default = 1).
-.TP
-\fB\-\-sccperc\fP = <\fInum\fP> [0-1]
-Perform SCC only if the number of new binary clauses is at least this
-percentage of the number of free variables (default = 0.02).
-.SS "COMPONENT"
-.TP
-\fB\-\-findcomp\fP = \fI{0,1}\fP
-Find components, but do not treat them (default = 0).
-.TP
-\fB\-\-comps\fP = \fI{0,1}\fP
-Perform component-finding and separate handling (default = 1).
-.TP
-\fB\-\-compsfrom\fP = <\fInum\fP>
-Do component finding only after this many simplification rounds (default = 0).
-.TP
-\fB\-\-compsvar\fP = <\fInum\fP>
-Only use components when the number of variables is below this limit
-(default = 1000000).
-.TP
-\fB\-\-compslimit\fP = <\fInum\fP>
-Limit how much time is spent in component finding (default = 500).
-.SS "XOR-RELATED"
-.TP
-\fB\-\-xor\fP = \fI{0,1}\fP
-Discover long XORs (default = 1).
-.TP
-\fB\-\-xorcache\fP = \fI{0,1}\fP
-Use cache when finding XORs (default = 0).  This finds a \fIlot\fP more XORs,
-but takes a lot more time.
-.TP
-\fB\-\-echelonxor\fP = \fI{0,1}\fP
-Extract data from XORs through echelonization \fIat the top level only\fP
-(default = 1).
-.TP
-\fB\-\-maxxormat\fP = <\fInum\fP>
-The maximum matrix size (i.e., number of elements) that we should try to
-echelonize (default = 10000000).
-.SS "GATE-RELATED"
-.TP
-\fB\-\-gates\fP = \fI{0,1}\fP
-Find gates (default = 1).  Disables all other gate-related sub-options.
-.TP
-\fB\-\-gorshort\fP = \fI{0,1}\fP
-Shorten clauses with OR gates (default = 1).
-.TP
-\fB\-\-gandrem\fP = \fI{0,1}\fP
-Remove clauses with AND gates (default = 1).
-.TP
-\fB\-\-gateeqlit\fP = \fI{0,1}\fP
-Find equivalent literals using gates (default = 1).
-.TP
-\fB\-\-printgatedot\fP = \fI{0,1}\fP
-Print gate structure regularly to the file 'gatesX.dot' (default = 0).
-.SS "SQL"
-.TP
-\fB\-\-sql\fP = \fI{0,1,2}\fP
-Write to SQL (default = 1).  0 means do not attempt to write to the database.
-1 means to try to write to the database, but continue if the attempt fails.  2
-means to abort if the database cannot be written.
-.TP
-\fB\-\-topnvars\fP = <\fInum\fP>
-At every restart, dump data about the top N variables (default = 0).  If set
-to 0, nothing is dumped.
-.TP
-\fB\-\-dumptreevar\fP = \fI{0,1}\fP
-Dump variance stats of the variables' decision and trail depths (default = 0).
-.TP
-\fB\-\-sqluser\fP = <\fIusername\fP>
-The SQL user to connect with (default = cmsat_solver).
-.TP
-\fB\-\-sqlpass\fP = <\fIpassword\fP>
-The SQL password to connect with.
-.TP
-\fB\-\-sqldb\fP = <\fIdatabase\fP>
-The SQL database name (default = cmsat).  The default is used by the PHP
-system, so it is highly recommended.
-.TP
-\fB\-\-sqlserver\fP = <\fIhostname\fP>
-The SQL server hostname or IP address (default = localhost).
-.SS "MISCELLANEOUS"
-.TP
-\fB\-\-vivif\fP = \fI{0,1}\fP
-Regularly execute clause vivification (default = 1).
-.TP
-\fB\-\-viviflongmaxm\fP = <\fInum\fP>
-Maximum time in mega-bogoprops to spend on vivifying long irreducible clauses
-by enqueueing and propagating (default = 20).
-.TP
-\fB\-\-viviffastmaxm\fP = <\fInum\fP>
-Maximum time in mega-bogoprops to spend on vivifying long irreducible clauses
-through watches, cache and stamps (default = 400).
-.TP
-\fB\-\-sortwatched\fP = \fI{0,1}\fP
-Sort watches according to size (default = 1).
-.TP
-\fB\-\-renumber\fP = \fI{0,1}\fP
-Renumber variables to increase CPU cache efficiency (default = 1).
-.TP
-\fB\-\-savemem\fP = \fI{0,1}\fP
-Save memory by deallocating variable space after renumbering (default = 1).
-This only works if renumbering is active.
-.TP
-\fB\-\-implicitmanip\fP = \fI{0,1}\fP
-Subsume and strengthen implicit clauses with each other (default = 1).
-.TP
-\fB\-\-implsubsto\fP = <\fInum\fP>
-The timeout of implicit subsumption in mega-bogoprops (default = 1900).
-.TP
-\fB\-\-burst\fP = <\fInum\fP>
-The number of conflicts to do in burst search (default = 300).
-.TP
-\fB\-\-clearinter\fP = \fI{0,1}\fP
-Interrupt threads cleanly, all the time (default = 0).
-.TP
-\fB\-\-zero\-exit\-status\fP = \fI{0,1}\fP
-Exit with status zero in case the solving has finished without an issue.
-.SH "EXIT STATUS"
-.PP
-The output is a solution, together with some timing information.  If
-\-\-zero\-exit\-status has not been specified, then the exit status is as
-follows:
-.IP 10
-The problem is satisfiable.
-.IP 15
-The problem's satisfiability was not determined.
-.IP 20
-The problem is unsatisfiable.
-.SH AUTHOR
-Mate Soos (soos(a)srlabs.de)
-.SH "SEE ALSO"
-The DIMACS input format can be looked up here:
-
-http://www.satcompetition.org/2009/format-benchmarks2009.html
diff --git a/cryptominisat4.spec b/cryptominisat4.spec
deleted file mode 100644
index 162f040..0000000
--- a/cryptominisat4.spec
+++ /dev/null
@@ -1,183 +0,0 @@
-Name:           cryptominisat4
-Version:        4.5.3
-Release:        16%{?dist}
-Summary:        SAT solver
-
-License:        LGPLv2
-URL:            http://www.msoos.org/cryptominisat4/
-Source0:        https://github.com/msoos/cryptominisat/archive/%{version}.tar.gz
-# Text is from the sources, therefore under the same copyright and license as
-# the code.  Man page formatting contributed by Jerry James.
-Source1:        %{name}.1
-# Fix failure to build from source due to incorrect return type.  Will not be
-# sent upstream, as upstream is on to major version 5 now.
-Patch0:         %{name}-heap.patch
-
-BuildRequires:  boost-devel
-BuildRequires:  chrpath
-BuildRequires:  cmake
-BuildRequires:  gcc-c++
-BuildRequires:  m4ri-devel
-BuildRequires:  python2-devel
-BuildRequires:  tbb-devel
-%ifnarch s390
-BuildRequires:  valgrind-devel
-%endif
-BuildRequires:  vim-common
-BuildRequires:  zlib-devel
-
-Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
-
-%description
-CryptoMiniSat is a modern, multi-threaded, feature-rich, simplifying SAT
-solver. Highlights:
-- Instance simplification at every point of the search (inprocessing)
-- Over 100 configurable parameters to tune to specific needs
-- Collection of statistical data to MySQL database + javascript-based
-  visualization of it
-- Clean C++ and python interfaces
-
-%package devel
-Summary:        Header files for developing with %{name}
-Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
-Requires:       m4ri-devel%{?_isa}
-Requires:       tbb-devel%{?_isa}
-
-%description devel
-Header files for developing applications that use %{name}.
-
-%package libs
-Summary:        Cryptominisat library
-
-%description libs
-The %{name} library.
-
-%package -n python2-%{name}
-%{?python_provide:%python_provide python2-%{name}}
-Summary:        Python interface to %{name}
-Requires:       %{name}-libs%{?_isa} = %{version}-%{release}
-
-%description -n python2-%{name}
-Python interface to %{name}.
-
-%prep
-%setup -q -n cryptominisat-%{version}
-%patch0
-
-# Don't override our compiler flags
-sed -i 's/-O2 -mtune=native/-DNDEBUG/' CMakeLists.txt
-if [ "%{_libdir}" = "%{_prefix}/lib64" ]; then
-  sed -i 's,${dir}/lib,&64,g' cmake/FindPkgMacros.cmake
-fi
-
-# Fix the python install
-sed -ri 's|install |&--root %{buildroot} |' python/CMakeLists.txt
-
-%build
-%cmake -DALSO_BUILD_STATIC_LIB=OFF .
-make %{?_smp_mflags}
-
-%install
-make install DESTDIR=%{buildroot}
-
-# Install the man page
-mkdir -p %{buildroot}%{_mandir}/man1
-sed 's/@VERSION@/%{version}/' %{SOURCE1} > \
-    %{buildroot}%{_mandir}/man1/%{name}.1
-touch -r %{SOURCE1} %{buildroot}%{_mandir}/man1/%{name}.1
-
-# Move library files to where they should go
-if [ "%{_libdir}" = "/usr/lib64" ]; then
-  mkdir -p %{buildroot}%{_libdir}
-  mv %{buildroot}%{_prefix}/lib/lib%{name}* %{buildroot}%{_libdir}
-  mv %{buildroot}%{_prefix}/lib/cmake %{buildroot}%{_libdir}
-  sed -i 's|%{_prefix}/lib/|%{_libdir}/|' \
-      %{buildroot}%{_libdir}/cmake/%{name}/*.cmake
-fi
-
-# Remove buildroot paths from cmake files
-sed -i 's|%{buildroot}||' %{buildroot}%{_libdir}/cmake/%{name}/*.cmake
-
-# Remove rpaths
-chrpath -d %{buildroot}%{_bindir}/%{name}
-chrpath -d %{buildroot}%{_bindir}/%{name}_simple
-
-# Fix permissions
-chmod 0755 %{buildroot}%{python2_sitearch}/pycryptosat.so
-
-%ldconfig_scriptlets
-
-%files
-%doc README.markdown
-%{_bindir}/%{name}
-%{_bindir}/%{name}_simple
-%{_mandir}/man1/%{name}*
-
-%files devel
-%{_includedir}/%{name}/
-%{_libdir}/lib%{name}.so
-%{_libdir}/cmake/*
-
-%files libs
-%doc AUTHORS
-%license LICENSE-LGPL
-%{_libdir}/lib%{name}.so.*
-
-%files -n python2-%{name}
-%doc python/README.rst
-%license python/LICENSE
-%{python2_sitearch}/pycryptosat*
-
-%changelog
-* Thu Jul 12 2018 Fedora Release Engineering <releng(a)fedoraproject.org&gt; - 4.5.3-16
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Wed Feb 07 2018 Fedora Release Engineering <releng(a)fedoraproject.org&gt; - 4.5.3-15
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Tue Jan 23 2018 Jonathan Wakely <jwakely(a)redhat.com&gt; - 4.5.3-14
-- Rebuilt for Boost 1.66
-
-* Sat Aug 19 2017 Zbigniew Jdrzejewski-Szmek <zbyszek(a)in.waw.pl&gt; - 4.5.3-13
-- Python 2 binary package renamed to python2-cryptominisat4
-  See https://fedoraproject.org/wiki/FinalizingFedoraSwitchtoPython3
-
-* Sun Aug 06 2017 Bjrn Esser <besser82(a)fedoraproject.org&gt; - 4.5.3-12
-- Rebuilt for AutoReq cmake-filesystem
-
-* Wed Aug 02 2017 Fedora Release Engineering <releng(a)fedoraproject.org&gt; - 4.5.3-11
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
-
-* Wed Jul 26 2017 Fedora Release Engineering <releng(a)fedoraproject.org&gt; - 4.5.3-10
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
-
-* Mon Jul 03 2017 Jonathan Wakely <jwakely(a)redhat.com&gt; - 4.5.3-9
-- Rebuilt for Boost 1.64
-
-* Mon May 15 2017 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org&gt; -
4.5.3-8
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_27_Mass_Rebuild
-
-* Tue Feb 07 2017 Kalev Lember <klember(a)redhat.com&gt; - 4.5.3-7
-- Rebuilt for Boost 1.63
-
-* Tue Jul 19 2016 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org&gt; -
4.5.3-6
-- https://fedoraproject.org/wiki/Changes/Automatic_Provides_for_Python_RPM_...
-
-* Wed Feb 03 2016 Fedora Release Engineering <releng(a)fedoraproject.org&gt; - 4.5.3-5
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
-
-* Fri Jan 15 2016 Jonathan Wakely <jwakely(a)redhat.com&gt; - 4.5.3-4
-- Rebuilt for Boost 1.60
-
-* Fri Sep 04 2015 Jonathan Wakely <jwakely(a)redhat.com&gt; - 4.5.3-3
-- Rebuilt for Boost 1.59
-
-* Fri Aug 28 2015 Jerry James <loganjerry(a)gmail.com&gt; - 4.5.3-2
-- Fix license
-- Also remove rpath from cryptominisat4_simple
-
-* Fri Aug 28 2015 Jerry James <loganjerry(a)gmail.com&gt; - 4.5.3-1
-- New upstream version
-
-* Sat Aug 22 2015 Jerry James <loganjerry(a)gmail.com&gt; - 4.5.2-1
-- Initial RPM
diff --git a/dead.package b/dead.package
new file mode 100644
index 0000000..b52ee31
--- /dev/null
+++ b/dead.package
@@ -0,0 +1 @@
+Obsoleted by cryptominisat (version 5.x)
diff --git a/sources b/sources
deleted file mode 100644
index a5c71c6..0000000
--- a/sources
+++ /dev/null
@@ -1 +0,0 @@
-7ad723a166409ef567224dd45554c45e  4.5.3.tar.gz