diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 23:12:00 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 23:12:00 +0100 |
| commit | 6f4e3de82246a4fe8b431e704e0e362b81c9f065 (patch) | |
| tree | b268ebf957f9d71c87c134b5106fb96dc3a7412e | |
| parent | 742f658b7aac7fab95416c7081be173b3393ad5a (diff) | |
| download | smtcoq-6f4e3de82246a4fe8b431e704e0e362b81c9f065.tar.gz smtcoq-6f4e3de82246a4fe8b431e704e0e362b81c9f065.zip | |
All tests (but large benchmarks) succeed
| -rw-r--r-- | unit-tests/Tests.v | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/unit-tests/Tests.v b/unit-tests/Tests.v index 3b8d95a..4a5b779 100644 --- a/unit-tests/Tests.v +++ b/unit-tests/Tests.v @@ -1,4 +1,3 @@ -(* Add LoadPath ".." as SMTCoq. *) Require Import SMTCoq. Require Import Bool PArray Int63 List ZArith. @@ -14,8 +13,8 @@ Time Zchaff_Checker "sat5.cnf" "sat5.zlog". Time Zchaff_Checker "sat6.cnf" "sat6.zlog". Time Zchaff_Checker "sat7.cnf" "sat7.zlog". Time Zchaff_Checker "hole4.cnf" "hole4.zlog". -Time Zchaff_Checker "cmu-bmc-barrel6.cnf" "cmu-bmc-barrel6.zlog". -Time Zchaff_Checker "velev-sss-1.0-05.cnf" "velev-sss-1.0-05.zlog". +(* Time Zchaff_Checker "cmu-bmc-barrel6.cnf" "cmu-bmc-barrel6.zlog". *) +(* Time Zchaff_Checker "velev-sss-1.0-05.cnf" "velev-sss-1.0-05.zlog". *) Time Zchaff_Theorem sat1 "sat1.cnf" "sat1.zlog". @@ -48,11 +47,11 @@ Compute Sat_Checker.checker d7 t7. Parse_certif_zchaff dhole4 thole4 "hole4.cnf" "hole4.zlog". Compute Sat_Checker.checker dhole4 thole4. -Parse_certif_zchaff dcmubmcbarrel6 tcmubmcbarrel6 "cmu-bmc-barrel6.cnf" "cmu-bmc-barrel6.zlog". -Compute Sat_Checker.checker dcmubmcbarrel6 tcmubmcbarrel6. +(* Parse_certif_zchaff dcmubmcbarrel6 tcmubmcbarrel6 "cmu-bmc-barrel6.cnf" "cmu-bmc-barrel6.zlog". *) +(* Compute Sat_Checker.checker dcmubmcbarrel6 tcmubmcbarrel6. *) -Parse_certif_zchaff dvelevsss1005 tvelevsss1005 "velev-sss-1.0-05.cnf" "velev-sss-1.0-05.zlog". -Compute Sat_Checker.checker dvelevsss1005 tvelevsss1005. +(* Parse_certif_zchaff dvelevsss1005 tvelevsss1005 "velev-sss-1.0-05.cnf" "velev-sss-1.0-05.zlog". *) +(* Compute Sat_Checker.checker dvelevsss1005 tvelevsss1005. *) (* zChaff tactic *) |