diff options
Diffstat (limited to 'examples/Example.v')
| -rw-r--r-- | examples/Example.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/examples/Example.v b/examples/Example.v index 806cd57..b83e619 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -19,7 +19,6 @@ Require Import SMTCoq.SMTCoq. Require Import Bool. Require Import ZArith. -Local Open Scope Z_scope. Import BVList.BITVECTOR_LIST. Local Open Scope bv_scope. @@ -27,10 +26,10 @@ Local Open Scope bv_scope. Import FArray. Local Open Scope farray_scope. -Local Open Scope int63_scope. - (* Examples that check ZChaff certificates *) +Local Open Scope int63_scope. + Zchaff_Checker "sat.cnf" "sat.log". Zchaff_Theorem sat "sat.cnf" "sat.log". Check sat. @@ -84,6 +83,8 @@ Proof. verit_bool. Qed. +Local Open Scope Z_scope. + Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b). Proof. |