summaryrefslogtreecommitdiffstats
path: root/src/sat
Commit message (Collapse)AuthorAgeFilesLines
* Enabling default no output in &icheck.Alan Mishchenko2014-02-151-0/+8
|
* Experiments with inductive don't-cares.Alan Mishchenko2014-02-112-3/+11
|
* Fixed problem with timeout in &bmc.Alan Mishchenko2013-12-181-0/+2
|
* Specialized inductive check.Alan Mishchenko2013-11-051-6/+3
|
* Specialized inductive check.Alan Mishchenko2013-11-051-1/+1
|
* Specialized inductive check.Alan Mishchenko2013-11-052-0/+140
|
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-052-2/+15
|
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-3/+3
|
* 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-043-2/+33
|
* Tuning for multi-ouptut solver.Alan Mishchenko2013-11-041-0/+2
|
* Added sharing of counter-examples across multiple failed properties in 'bmc3 ↵Alan Mishchenko2013-11-041-2/+2
| | | | -a'.
* Added sharing of counter-examples across multiple failed properties in 'bmc3 ↵Alan Mishchenko2013-11-041-1/+2
| | | | -a'.
* Merging heads.Alan Mishchenko2013-11-041-0/+5
|\
| * Specialized inductive check.Alan Mishchenko2013-11-041-0/+5
| |
* | Added sharing of counter-examples across multiple failed properties in 'bmc3 ↵Alan Mishchenko2013-11-041-43/+84
|/ | | | -a'.
* Sweeper condition complement bug-fix and code for internal verification.Alan Mishchenko2013-11-011-1/+1
|
* Specialized induction check.Alan Mishchenko2013-10-313-53/+132
|
* Specialized induction check.Alan Mishchenko2013-10-311-1/+5
|
* Specialized induction check.Alan Mishchenko2013-10-313-20/+98
|
* Specialized induction check.Alan Mishchenko2013-10-315-1/+201
|
* Wrapper around the BMC engine to restart it with higher resource limits.Alan Mishchenko2013-10-291-1/+38
|
* New BMC engine.Alan Mishchenko2013-10-272-2/+4
|
* New BMC engine.Alan Mishchenko2013-10-272-33/+36
|
* New BMC engine.Alan Mishchenko2013-10-271-1/+197
|
* Multi-output property solver.Alan Mishchenko2013-10-271-5/+6
|
* Getting rid of a recursive procedure during CNF construction in bmc3.Alan Mishchenko2013-10-271-8/+71
|
* Multi-output property solver.Alan Mishchenko2013-10-263-22/+44
|
* Multi-output property solver.Alan Mishchenko2013-10-261-15/+52
|
* Multi-output property solver.Alan Mishchenko2013-10-231-0/+204
|
* Multi-output property solver.Alan Mishchenko2013-10-233-1/+4
|
* Adding new synthesis scripts.Alan Mishchenko2013-10-231-2/+1
|
* Bug with in bmc3 when no 'sat' outputs are found and H != 0Alan Mishchenko2013-10-081-0/+2
|
* Integrating synthesis into the new BMC engine.Alan Mishchenko2013-10-021-4/+2
|
* Integrating synthesis into the new BMC engine.Alan Mishchenko2013-10-021-6/+8
|
* Integrating synthesis into the new BMC engine.Alan Mishchenko2013-10-022-0/+8
|
* Enabling counter-example generation in the new BMC engine.Alan Mishchenko2013-10-021-21/+24
|
* Enabling counter-example generation in the new BMC engine.Alan Mishchenko2013-10-011-12/+57
|
* 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-172-0/+13
|
* Compiler warning about unused variable.Alan Mishchenko2013-09-171-2/+2
|
* Changing dynamic CNF loading code to perform loading before propagate() as ↵Alan Mishchenko2013-09-161-0/+31
| | | | opposed to when the literal first implied in enqueue().
* Corrected variable naming in clause2_proofid().Alan Mishchenko2013-09-111-1/+1
|
* Updates for the new BMC engine.Alan Mishchenko2013-09-101-10/+16
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 19:20:08 +0000