summaryrefslogtreecommitdiffstats
path: root/src/proof
Commit message (Expand)AuthorAgeFilesLines
...
* Adding CEC command &splitprove.Alan Mishchenko2014-06-041-6/+7
* Adding CEC command &splitprove.Alan Mishchenko2014-06-041-9/+42
* Adding CEC command &splitprove.Alan Mishchenko2014-06-041-52/+59
* Adding CEC command &splitprove.Alan Mishchenko2014-06-041-2/+1
* Adding CEC command &splitprove.Alan Mishchenko2014-06-041-1/+1
* Adding CEC command &splitprove.Alan Mishchenko2014-06-041-46/+108
* Adding CEC command &splitprove.Alan Mishchenko2014-06-021-8/+9
* Adding CEC command &splitprove.Alan Mishchenko2014-06-021-0/+1
* Adding CEC command &splitprove.Alan Mishchenko2014-06-021-20/+160
* Code to explore cofactors of CEC problems.Alan Mishchenko2014-06-021-0/+213
* Adding switch to handle only single faults.Alan Mishchenko2014-04-011-1/+1
* Compiler warnings.Alan Mishchenko2014-03-311-1/+1
* Undoing previous change, which was made by mistake.Alan Mishchenko2014-03-311-1/+1
* Making per-output timeout in bmc3 -a and pdr -a work in CLOCKS_PER_SECs ins...Alan Mishchenko2014-03-311-1/+1
* Adding new code to verify invariant derived by 'pdr'.Alan Mishchenko2014-03-302-1/+83
* Synchronizing with the recent version.Alan Mishchenko2014-03-161-2/+2
* Significant improvement to LUT mappers (if, &if).Alan Mishchenko2014-02-161-1/+1
* Handing trivially UNSAT outputs in 'pdr'.Alan Mishchenko2014-02-131-0/+10
* Initial new interpolation code.Alan Mishchenko2014-01-287-0/+1254
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-051-1/+1
* Sweeper internal verification.Alan Mishchenko2013-11-011-1/+1
* Sweeper internal verification and new switch for &cfraig.Alan Mishchenko2013-11-012-2/+9
* Sweeper internal verification.Alan Mishchenko2013-11-011-0/+43
* Sweeper condition complement bug-fix and code for internal verification.Alan Mishchenko2013-11-011-1/+1
* Sweeper assertion.Alan Mishchenko2013-11-011-0/+2
* Sweeper assertion.Alan Mishchenko2013-11-011-0/+1
* Sweeper return value normalization.Alan Mishchenko2013-11-012-7/+17
* Multi-output property solver.Alan Mishchenko2013-10-261-0/+2
* Multi-output property solver.Alan Mishchenko2013-10-261-2/+2
* Multi-output property solver.Alan Mishchenko2013-10-232-0/+13
* Compiler warnings.Alan Mishchenko2013-10-173-4/+6
* Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe.Alan Mishchenko2013-10-152-4/+4
* Extending truth table support in &jf for more than 6 inputs.Alan Mishchenko2013-10-101-3/+3
* Compiler warning.Alan Mishchenko2013-10-051-69/+5
* Compiler warning.Alan Mishchenko2013-10-051-1/+1
* Added 'abort' message in bridge mode for pdr -a timeoutNiklas Een2013-10-041-34/+95
* Changing switch -R <num> in &gla to mean the max allowed size of abstraction....Alan Mishchenko2013-09-232-9/+10
* Adding resource limit to stop &gla when the number of remaining objects is le...Alan Mishchenko2013-09-211-0/+8
* Adding switch to enable reuse of proof-obligations in the last timeframe.Alan Mishchenko2013-09-162-1/+2
* Added bridge integration for multi-output 'pdr -a'.Alan Mishchenko2013-09-162-3/+18
* Bug fix in PDR.Alan Mishchenko2013-09-161-1/+1
* Fixing return value of 'pdr -a'.Alan Mishchenko2013-09-151-1/+5
* Handling the case when all outputs are undecided in 'pdr -a' with per-output ...Alan Mishchenko2013-09-142-6/+3
* Fixing several bugs, which led to unsound results produced by 'pdr -a' with p...Alan Mishchenko2013-09-133-4/+15
* Enabling additional printouts in 'pdr'.Alan Mishchenko2013-09-131-2/+4
* New API to return the set of all reachable states as an AIG.Alan Mishchenko2013-09-101-1/+93
* Unifying parameters for the &ps command.Alan Mishchenko2013-09-054-11/+11
* Adding procedures to specify permutations with unused flops.Alan Mishchenko2013-08-281-3/+12
* Added switch &sim -g to enable flop grouping.Alan Mishchenko2013-08-202-1/+38
* Experiment with 'pdr'.Alan Mishchenko2013-07-193-34/+126