diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-28 16:20:30 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-28 16:20:30 +0100 |
| commit | a25181f93604e279b899552b119d68df0c63b0ad (patch) | |
| tree | fcf69e5cdd62346b9d67a5c2e3bdb60eb0b0d8c3 /examples | |
| parent | f479497576c11bc0fcc116ede778d1744be6d78e (diff) | |
| download | smtcoq-a25181f93604e279b899552b119d68df0c63b0ad.tar.gz smtcoq-a25181f93604e279b899552b119d68df0c63b0ad.zip | |
Re-fixes in Example.v
Diffstat (limited to 'examples')
| -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. |