From 6f4e3de82246a4fe8b431e704e0e362b81c9f065 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 11 Feb 2015 23:12:00 +0100 Subject: All tests (but large benchmarks) succeed --- unit-tests/Tests.v | 13 ++++++------- 1 file 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 *) -- cgit