summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcBmc3.c
Commit message (Expand)AuthorAgeFilesLines
* Correctly updating the failed output when recording the CEX in bmc3 -a.Alan Mishchenko2020-04-031-1/+5
* Adding global conflict counter to Satoko (to make it apple-to-apple with othe...Alan Mishchenko2017-09-061-2/+4
* Integrating Glucose into bmc3 -g.Alan Mishchenko2017-09-061-9/+57
* Fixing bronken C++ build; Satoko internal header, solver.h, should not be use...Bruno Schmitt2017-08-291-15/+14
* Adding an option to bmc3 to use Satoko intead of the default SAT solver.Alan Mishchenko2017-08-161-34/+35
* Adding an option to bmc3 to use Satoko intead of the default SAT solver.Alan Mishchenko2017-08-131-45/+121
* added callbacks to bmc3 and sat solverYen-Sheng Ho2017-03-201-0/+2
* %pdra: working on bmc3Yen-Sheng Ho2017-03-191-0/+6
* Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.Alan Mishchenko2016-05-191-0/+1
* Bug fix in bmc3 -a -x.Alan Mishchenko2014-10-281-1/+1
* Bug fix in bmc3 -a -x.Alan Mishchenko2014-10-281-1/+1
* Updating logic file print-out.Alan Mishchenko2014-03-311-1/+3
* Undoing previous change, which was made by mistake.Alan Mishchenko2014-03-311-2/+2
* Making per-output timeout in bmc3 -a and pdr -a work in CLOCKS_PER_SECs ins...Alan Mishchenko2014-03-311-2/+2
* Adding new code to verify invariant derived by 'pdr'.Alan Mishchenko2014-03-301-2/+4
* Updating &if for new cut function representation.Alan Mishchenko2014-03-291-1/+1
* Adding per-output logging to bmc3.Alan Mishchenko2014-03-291-6/+13
* Compiler warning.Alan Mishchenko2014-03-181-1/+1
* Adding special-case report to 'bmc3'.Alan Mishchenko2014-03-181-0/+6
* Adding progress report to 'bmc3'.Alan Mishchenko2014-03-171-0/+10
* Bug fix in multi-output BMC.Alan Mishchenko2014-03-111-0/+2
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-7/+0
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-1/+1
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-1/+5
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-0/+2
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-0/+1
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-1/+1
* Added sharing of counter-examples across multiple failed properties in 'bmc3 ...Alan Mishchenko2013-11-041-2/+2
* Added sharing of counter-examples across multiple failed properties in 'bmc3 ...Alan Mishchenko2013-11-041-1/+2
* Added sharing of counter-examples across multiple failed properties in 'bmc3 ...Alan Mishchenko2013-11-041-43/+84
* Getting rid of a recursive procedure during CNF construction in bmc3.Alan Mishchenko2013-10-271-8/+71
* Multi-output property solver.Alan Mishchenko2013-10-261-1/+1
* Multi-output property solver.Alan Mishchenko2013-10-231-1/+2
* Bug with in bmc3 when no 'sat' outputs are found and H != 0Alan Mishchenko2013-10-081-0/+2
* Compiler warnings.Alan Mishchenko2013-09-251-2/+10
* Fixing printouts in 'bmc3'.Alan Mishchenko2013-09-251-58/+58
* Added bridge integration for multi-output 'bmc3 -a'.Alan Mishchenko2013-09-171-8/+5
* Added bridge integration for multi-output 'bmc3 -a'.Alan Mishchenko2013-09-171-0/+12
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-271-1/+1
* Adding a wrapper around clock() for more accurate time counting in ABC.Alan Mishchenko2013-05-271-32/+32
* Improvements to 'bmc3'.Alan Mishchenko2013-05-181-158/+11
* SAT variable profiling.Alan Mishchenko2013-05-181-5/+53
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+1
* SAT variable profiling.Alan Mishchenko2013-05-181-3/+9
* SAT variable profiling.Alan Mishchenko2013-05-181-2/+8
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+1
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-3/+0
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+3
* SAT variable profiling (undo).Alan Mishchenko2013-05-181-3/+0
* SAT variable profiling.Alan Mishchenko2013-05-181-0/+3