aboutsummaryrefslogtreecommitdiffstats
path: root/unit-tests/Tests_verit.v
Commit message (Collapse)AuthorAgeFilesLines
* Compatibility with native-coqChantal Keller2016-04-261-8/+8
|
* - Solved the Coq 8.5 problem relating to declaring section variablesChantal Keller2016-04-261-3/+3
| | | | - Correct equality check of atoms and formulas for processing congruence closure
* The simplest test for SMTChantal Keller2016-04-241-0/+13
|
* New targets [make vtest] and [make ztest] to perform unit tests for the ↵Chantal Keller2016-03-021-0/+862
various solvers separately