Merge from LFSC (#26)

* Showing models as coq counter examples in tactic without constructing coq terms

* also read models when calling cvc4 with a file (deactivated because cvc4 crashes)

* Show counter examples with variables in the order they are quantified in the Coq goal

* Circumvent issue with ocamldep

* fix issue with dependencies

* fix issue with dependencies

* Translation and OCaml support for extract, zero_extend, sign_extend

* Show run times of components

* print time on stdout instead

* Tests now work with new version (master) of CVC4

* fix small printing issue

* look for date on mac os x

* proof of valid_check_bbShl: some cases to prove.

* full proof of "left shift checker".

*  full proof of "rigth shift checker".

* Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment
Bug fix for bitvector extract (inverted arguments)

* Typo

* More modularity on the format of traces depending on the version of coq

* More straightforward definitions in Int63Native_standard

* Use the Int31 library with coq-8.5

* Use the most efficient operations of Int31

* Improved performance with coq-8.5

* Uniform treatment of sat and smt tactics

* Hopefully solved the problem with universes for the tactic

* Updated the installation instructions

* Holes for unsupported bit blasting rules

* Cherry-picking from smtcoq/smtcoq

* bug fix hole for bitblast

* Predefined arrays are not required anymore

* fix issue with coq bbT and bitof construction from ocaml

* bug fix in smtAtom for uninterpreted functions
fix verit test file

* fix issue with smtlib2 extract parsing

* It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2)

* Solver specific reification:
Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features.

* show counter-examples with const_farray instead of const for constant array definitions

* Vernacular commands to debug checkers.
Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked

* Update INSTALL.md

* show smtcoq proof when converting

* (Hopefully) repared the universes problems

* Corrected a bug with holes in proofs

* scripts for tests:
create a folder "work" under "lfsc/tests/", locate the benchmarks there.
create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq.

* make sure to give correct path for your benchs...

* Checker for array extensionality modulo symmetry of equality

* fix oversight with bitvectors larger than 63 bits

* some printing functions for smt2 ast

* handle smtlib2 files with more complicated equivalence with (= ... )

* revert: ./cvc4tocoq does not output lfsc proofs...

* bug fix one input was ignored

* Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set
(e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile)

* Also sort names of introduced variables when showing counter-example

* input files for which SMTCoq retuns false.

* input files for which SMTCoq retuns false.

* use debug checker for debug file

* More efficient debug checker

* better approximate number of failing step of certificate in debug checker

* fix mistake in ml4

* very first attempt to support goals in Prop

* bvs: comparison predicates in Prop and their <-> proofs with the ones in bool
farrays: equality predicate in Prop and its <-> proof with the one in bool.

* unit, Bool, Z, Pos: comparison and equality predicates in Prop.

* a typo fixed.

* an example of array equality in  Prop (converted into Bool by hand)...
TODO: enhance the search space of cvc4 tactic.

* first version of cvc4' tactic: "solves" the goals in Prop.
WARNING: supports only bv and array goals and might not be complete
TODO: add support for lia goals

* cvc4' support for lia
WARNING: might not be complete!

* small fix in cvc4' and some variations of examples

* small fix + support for goals in Bool and Bool = true + use of solve tactical
WARNING: does not support UF and INT63 goals in Prop

* cvc4': better arrangement

* cvc4': Prop2Bool by context search...

* cvc4': solve tactial added -> do not modify unsolved goals.

* developer documentation for the smtcoq repo

* cvc4': rudimentary support for uninterpreted function goals in Prop.

* cvc4': support for goals with Leibniz equality...
WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays!

* cvc4': Z.lt adapted + better support from verit...

* cvc4': support for Z.le, Z.ge, Z.gt.

* Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable

* cvc4': support for equality over uninterpreted types

* lfsc demo: goals in Coq's Prop.

* lfsc demo: goals in Bool.

* Fix issue with existential variables generated by prop2bool.
- prop2bool tactic exported by SMTCoq
- remove useless stuff

* update usage and installation instructions

* Update INSTALL.md

* highlighting

* the tactic: bool2prop.

* clean up

* the tactic smt: very first version.

* smt: return unsolved goals in Prop.

* Show when a certificate cannot be checked when running the tactic instead of at Qed

* Tactic improvements
- Handle negation/True/False in prop/bool conversions tactic.
- Remove alias for farray (this caused problem for matching on this type in tactics).
- Tactic `smt` that combines cvc4 and veriT.
- return subgoals in prop

* test change header

* smt: support for negated goals + some reorganization.

* conflicts resolved + some reorganization.

* a way to solve the issue with ambiguous coercions.

* reorganization.

* small change.

* another small change.

* developer documentation of the tactics.

* developer guide: some improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* developer guide: some more improvements.

* pass correct environment for conversion + better error messages

* cleaning

* ReflectFacts added.

* re-organizing developers' guide.

* re-organizing developers' guide.

* re-organizing developers' guide.

* removing unused maps.

* headers.

* artifact readme getting started...

* first attempt

* second...

* third...

* 4th...

* 5th...

* 6th...

* 7th...

* 8th...

* 9th...

* 10th...

* 11th...

* 12th...

* 13th...

* 14th...

* 15th...

* 16th...

* 17th...

* Update artifact.md

Use links to lfsc repository like in the paper

* 18th...

* 19th...

* 20th...

* 21st...

* 22nd...

* 23rd...

* 24th...

* 25th...

* 26th...

* 27th...

* 28th...

* Update artifact.md

Small reorganization

* minor edits

* More minor edits

* revised description of tactics

* Final pass

* typo

* name changed: artifact-readme.md

* file added...

* passwd chaged...

* links...

* removal

* performance statement...

* typos...

* the link to the artifact image updated...

* suggestions by Guy...

* aux files removed...

* clean-up...

* clean-up...

* some small changes...

* small fix...

* additional information on newly created files after running cvc4tocoq script...

* some small fix...

* another small fix...

* typo...

* small fix...

* another small fix...

* fix...

* link to the artifact image...

* We do not want to force vm_cast for the Theorem commands

* no_check variants of the tactics

* TODO: a veriT test does not work anymore

* Compiles with both versions of Coq

* Test of the tactics in real conditions

* Comment on this case study

* an example for the FroCoS paper.

* Fix smt tactic that doesn't return cvc4's subgoals

* readme modifications

* readme modifications 2

* small typo in readme.

* small changes in readme.

* small changes in readme.

* typo in readme.

* Sync with https://github.com/LFSC/smtcoq

* Port to Coq 8.6

* README

* README

* INSTALL

* Missing file

* Yves' proposition for installation instructions

* Updated link to CVC4

* Compiles again with native-coq

* Compiles with both versions of Coq

* Command to bypass typechecking when generating a zchaff theorem

* Solved bug on cuts from Hole

* Counter-models for uninterpreted sorts (improves issue #13)

* OCaml version note (#15)

* update .gitignore

* needs OCaml 4.04.0

* Solving merge issues (under progress)

* Make SmtBtype compile

* Compilation of SmtForm under progress

* Make SmtForm compile

* Make SmtCertif compile

* Make SmtTrace compile

* Make SatAtom compile

* Make smtAtom compile

* Make CnfParser compile

* Make Zchaff compile

* Make VeritSyntax compile

* Make VeritParser compile

* Make lfsc/tosmtcoq compile

* Make smtlib2_genconstr compile

* smtCommand under progress

* smtCommands and verit compile again

* lfsc compiles

* ml4 compiles

* Everything compiles

* All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through

* Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate

* Authors and headings

* Compiles with native-coq

* Typo

14 files changed, 1400 insertions, 47 deletions

diff --git a/unit-tests/Makefile b/unit-tests/Makefile
index bed1018..1ad9b57 100644
--- a/unit-tests/Makefile
+++ b/unit-tests/Makefile
@@ -10,9 +10,10 @@ COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
 COQC?=$(COQBIN)coqc
 
 
-all: $(OBJ) Tests_zchaff.vo Tests_verit.vo
+all: zchaff verit lfsc
 zchaff: $(ZCHAFFLOG) Tests_zchaff.vo
 verit: $(VERITLOG) Tests_verit.vo
+lfsc: Tests_lfsc.vo
 logs: $(OBJ)
 
 
diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v
new file mode 100644
index 0000000..9734fde
--- /dev/null
+++ b/unit-tests/Tests_lfsc.v
@@ -0,0 +1,700 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Add Rec LoadPath "../src" as SMTCoq.
+
+Require Import SMTCoq.
+Require Import Bool PArray Int63 List ZArith Logic.
+
+
+Infix "-->" := implb (at level 60, right associativity) : bool_scope.
+
+
+Section BV.
+
+Import BVList.BITVECTOR_LIST.
+Local Open Scope bv_scope.
+
+  Goal forall (a b c: bitvector 4),
+                                 (c = (bv_and a b)) ->
+                                 ((bv_and (bv_and c a) b) = c).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (bv1 bv2 bv3: bitvector 4),
+      bv1 = #b|0|0|0|0|  /\
+      bv2 = #b|1|0|0|0|  /\
+      bv3 = #b|1|1|0|0|  ->
+      bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3.
+  Proof. 
+     smt.
+  Qed.
+
+
+  Goal forall (a: bitvector 32), a = a.
+  Proof.
+    smt.
+  Qed.
+
+  (* TODO: will be ok when symmetry of equality is back for verit *)
+  (* Goal forall (bv1 bv2: bitvector 4), *)
+  (*      bv1 = bv2 <-> bv2 = bv1. *)
+  (* Proof. *)
+  (*    smt. *)
+  (* Qed. *)
+
+End BV.
+
+
+Section Arrays.
+
+  Import FArray.
+  Local Open Scope farray_scope.
+
+
+  Goal forall (a:farray Z Z) i j, i = j -> a[i] = a[j].
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: farray Z Z)
+         (v w x y: Z)
+         (g: farray Z Z -> Z)
+         (f: Z -> Z),
+         (a[x <- v] = b) /\ a[y <- w] = b  ->
+         (f x) = (f y) \/  (g a) = (g b).
+  Proof.
+    smt.
+  Qed.
+
+
+  (* TODO *)
+  (* Goal forall (a b c d: farray Z Z), *)
+  (*     b[0%Z <- 4] = c  -> *)
+  (*     d = b[0%Z <- 4][1%Z <- 4]  -> *)
+  (*     a = d[1%Z <- b[1%Z]]  -> *)
+  (*     a = c. *)
+  (* Proof. *)
+  (*   smt. *)
+  (* Qed. *)
+
+
+(*
+  Goal forall (a b: farray Z Z) i,
+      (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) =  4.
+  Proof.
+    smt.
+    rewrite read_over_other_write; try easy.
+    rewrite read_over_same_write; try easy; try apply Z_compdec.
+    rewrite read_over_same_write; try easy; try apply Z_compdec.
+  Qed.
+*)
+
+
+End Arrays.
+
+
+Section EUF.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         y = x -> (f x) = (f y).
+  Proof.
+    smt.
+  Qed.
+
+  (* TODO: will be ok when symmetry of equality is back for verit *)
+  (* Goal forall *)
+  (*        (x y: Z) *)
+  (*        (f: Z -> Z), *)
+  (*        (f x) = (f y) -> (f y) = (f x). *)
+  (* Proof. *)
+  (*   smt. *)
+  (* Qed. *)
+
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         x + 1 = (y + 1) -> (f y) = (f x).
+  Proof.
+    smt.
+  Qed.
+
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         x = (y + 1) -> (f y) = (f (x - 1)).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         x = (y + 1) -> (f (y + 1)) = (f x).
+  Proof.
+    smt.
+  Qed.
+
+End EUF.
+
+
+Section LIA.
+
+
+  (* TODO: will be ok when symmetry of equality is back for verit *)
+  (* Goal forall (a b: Z), a = b <-> b = a. *)
+  (* Proof. *)
+  (*   smt. *)
+  (* Qed. *)
+
+  Goal forall (x y: Z), (x >= y) -> (y < x) \/ (x = y).
+  Proof. 
+    smt. 
+  Qed.
+
+
+  Goal forall (f : Z -> Z) (a:Z), ((f a) > 1) ->  ((f a) + 1) >= 2 \/((f a) = 30) .
+  Proof.
+   smt.
+  Qed.
+ 
+  Goal forall x: Z, (x = 0%Z) -> (8 >= 0).
+  Proof.
+    smt.
+   Qed.
+
+  Goal forall x: Z, ~ (x < 0%Z) -> (8 >= 0).
+  Proof. 
+    smt. 
+  Qed.
+
+  Goal forall (a b: Z), a < b -> a < (b + 1).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: Z), (a < b) -> (a + 2) < (b + 3).
+  Proof.
+    smt.
+  Qed.
+
+
+  Goal forall a b, a < b -> a < (b + 10).
+  Proof. 
+    smt.
+  Qed.
+
+
+End LIA.
+
+
+Section PR.
+
+ Local Open Scope int63_scope.
+
+(* Simple connectors *)
+
+Goal forall (a:bool), a || negb a.
+  smt.
+Qed.
+
+Goal forall a, negb (a || negb a) = false.
+  smt.
+Qed.
+
+Goal forall a, (a && negb a) = false.
+  smt.
+Qed.
+
+Goal forall a, negb (a && negb a).
+  smt.
+Qed.
+
+Goal forall a, a --> a.
+  smt.
+Qed.
+
+Goal forall a, negb (a --> a) = false.
+  smt.
+Qed.
+
+
+Goal forall a , (xorb a a) || negb (xorb a a).
+  smt.
+Qed.
+
+
+Goal forall a, (a||negb a) || negb (a||negb a).
+  smt.
+Qed.
+
+(* Polarities *)
+
+Goal forall a b, andb (orb (negb (negb a)) b) (negb (orb a b)) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false.
+Proof.
+  smt.
+Qed.
+
+(* Multiple negations *)
+
+Goal forall a, orb a (negb (negb (negb a))) = true.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c,
+  (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal true.
+  smt.
+Qed.
+
+Goal negb false.
+  smt.
+Qed.
+
+ 
+Goal forall a, Bool.eqb a a.
+Proof.
+  smt.
+Qed.
+
+ 
+Goal forall (a:bool), a = a.
+  smt.
+Qed.
+
+Goal (false || true) && false = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal negb true = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal false = false.
+Proof.
+  smt.
+Qed.
+
+Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)).
+Proof.
+  smt.
+Qed.
+
+
+Goal forall x y, Bool.eqb (x --> y) ((x && y) || (negb x)).
+Proof.
+  smt.
+Qed.
+
+
+Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)).
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false.
+Proof.
+  smt.
+Qed.
+
+Goal forall a, ((a || a) && (negb a)) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a, (negb (a || (negb a))) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c,
+  (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
+Proof.
+  smt.
+Qed.
+
+
+(** The same goal above with a, b and c are concrete terms *)
+Goal forall i j k,
+  let a := i == j in
+  let b := j == k in
+  let c := k == i in
+  (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false.
+Proof.
+  smt.
+Qed.
+
+
+(* Pigeon hole: 4 holes, 5 pigeons *)
+Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 x43 x44 x45, (
+  (orb (negb x11) (negb x21)) &&
+  (orb (negb x11) (negb x31)) &&
+  (orb (negb x11) (negb x41)) &&
+  (orb (negb x21) (negb x31)) &&
+  (orb (negb x21) (negb x41)) &&
+  (orb (negb x31) (negb x41)) &&
+
+  (orb (negb x12) (negb x22)) &&
+  (orb (negb x12) (negb x32)) &&
+  (orb (negb x12) (negb x42)) &&
+  (orb (negb x22) (negb x32)) &&
+  (orb (negb x22) (negb x42)) &&
+  (orb (negb x32) (negb x42)) &&
+
+  (orb (negb x13) (negb x23)) &&
+  (orb (negb x13) (negb x33)) &&
+  (orb (negb x13) (negb x43)) &&
+  (orb (negb x23) (negb x33)) &&
+  (orb (negb x23) (negb x43)) &&
+  (orb (negb x33) (negb x43)) &&
+
+  (orb (negb x14) (negb x24)) &&
+  (orb (negb x14) (negb x34)) &&
+  (orb (negb x14) (negb x44)) &&
+  (orb (negb x24) (negb x34)) &&
+  (orb (negb x24) (negb x44)) &&
+  (orb (negb x34) (negb x44)) &&
+
+  (orb (negb x15) (negb x25)) &&
+  (orb (negb x15) (negb x35)) &&
+  (orb (negb x15) (negb x45)) &&
+  (orb (negb x25) (negb x35)) &&
+  (orb (negb x25) (negb x45)) &&
+  (orb (negb x35) (negb x45)) &&
+
+
+  (orb (negb x11) (negb x12)) &&
+  (orb (negb x11) (negb x13)) &&
+  (orb (negb x11) (negb x14)) &&
+  (orb (negb x11) (negb x15)) &&
+  (orb (negb x12) (negb x13)) &&
+  (orb (negb x12) (negb x14)) &&
+  (orb (negb x12) (negb x15)) &&
+  (orb (negb x13) (negb x14)) &&
+  (orb (negb x13) (negb x15)) &&
+  (orb (negb x14) (negb x15)) &&
+
+  (orb (negb x21) (negb x22)) &&
+  (orb (negb x21) (negb x23)) &&
+  (orb (negb x21) (negb x24)) &&
+  (orb (negb x21) (negb x25)) &&
+  (orb (negb x22) (negb x23)) &&
+  (orb (negb x22) (negb x24)) &&
+  (orb (negb x22) (negb x25)) &&
+  (orb (negb x23) (negb x24)) &&
+  (orb (negb x23) (negb x25)) &&
+  (orb (negb x24) (negb x25)) &&
+
+  (orb (negb x31) (negb x32)) &&
+  (orb (negb x31) (negb x33)) &&
+  (orb (negb x31) (negb x34)) &&
+  (orb (negb x31) (negb x35)) &&
+  (orb (negb x32) (negb x33)) &&
+  (orb (negb x32) (negb x34)) &&
+  (orb (negb x32) (negb x35)) &&
+  (orb (negb x33) (negb x34)) &&
+  (orb (negb x33) (negb x35)) &&
+  (orb (negb x34) (negb x35)) &&
+
+  (orb (negb x41) (negb x42)) &&
+  (orb (negb x41) (negb x43)) &&
+  (orb (negb x41) (negb x44)) &&
+  (orb (negb x41) (negb x45)) &&
+  (orb (negb x42) (negb x43)) &&
+  (orb (negb x42) (negb x44)) &&
+  (orb (negb x42) (negb x45)) &&
+  (orb (negb x43) (negb x44)) &&
+  (orb (negb x43) (negb x45)) &&
+  (orb (negb x44) (negb x45)) &&
+
+
+  (orb (orb (orb x11 x21) x31) x41) &&
+  (orb (orb (orb x12 x22) x32) x42) &&
+  (orb (orb (orb x13 x23) x33) x43) &&
+  (orb (orb (orb x14 x24) x34) x44) &&
+  (orb (orb (orb x15 x25) x35) x45)) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c f p, ((Z.eqb a c) && (Z.eqb b c) && ((negb (Z.eqb (f a) (f b))) || ((p a) && (negb (p b))))) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall x y z f, ((Z.eqb x y) && (Z.eqb y z) && (negb (Z.eqb (f x) (f z)))) = false.
+Proof.
+  smt.
+Qed.
+
+Goal forall x y z f, ((negb (Z.eqb (f x) (f y))) && (Z.eqb y z) && (Z.eqb (f x) (f (f z))) && (Z.eqb x y)) = false.
+Proof.
+  smt.
+Qed.
+
+Goal forall a b c d e f, ((Z.eqb a b) && (Z.eqb b c) && (Z.eqb c d) && (Z.eqb c e) && (Z.eqb e f) && (negb (Z.eqb a f))) = false.
+Proof.
+  smt.
+Qed.
+
+
+
+Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9))) -->
+  ((x + y <=? 10) || (x + z <=? 12)) = true.
+Proof.
+  smt.
+Qed.
+
+Goal forall x, (Z.eqb (x - 3) 7)  -->  (x >=? 10) = true.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall x y, (x >? y) --> (y + 1 <=? x) = true.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true.
+Proof.
+  smt.
+Qed.
+
+Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) 
+        || (x <=? - (3))) && (x >=? 0) = false. 
+ Proof. 
+   smt.
+ Qed. 
+
+Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3))) --> (x >=? 10) = true.
+Proof.
+  smt.
+Qed.
+
+Goal forall x, (Z.eqb (x - 3) 7) --> (10 <=? x) = true.
+Proof.
+  smt.
+Qed.
+
+
+(* More general examples *)
+Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false.
+Proof.
+  smt.
+Qed.
+
+
+Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
+  (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b).
+Proof.
+  smt.
+Qed.
+
+
+Goal forall b1 b2 x1 x2,
+  (ifb b1
+    (ifb b2 (Z.eqb (2*x1+1) (2*x2+1)) (Z.eqb (2*x1+1) (2*x2)))
+    (ifb b2 (Z.eqb (2*x1) (2*x2+1)) (Z.eqb (2*x1) (2*x2)))) -->
+  ((b1 --> b2) && (b2 --> b1) && (Z.eqb x1 x2)).
+Proof.
+  smt.
+Qed.
+
+
+(* With let ... in ... *)
+Goal forall b,
+  let a := b in
+  a && (negb a) = false.
+Proof.
+  smt.
+Qed.
+
+Goal forall b,
+  let a := b in
+  a || (negb a) = true.
+Proof.
+  smt.
+Qed.
+
+(* With concrete terms *)
+Goal forall i j,
+  let a := i == j in
+  a && (negb a) = false.
+Proof.
+  smt.
+Qed.
+
+Goal forall i j,
+  let a := i == j in
+  a || (negb a) = true.
+Proof.
+  smt.
+Qed.
+
+
+(* Congruence in which some premises are REFL *)
+Goal forall (f:Z -> Z -> Z) x y z,
+  (Z.eqb x y) --> (Z.eqb (f z x) (f z y)).
+Proof.
+  smt.
+Qed.
+
+Goal forall (f:Z -> Z -> Z) x y z,
+  (x = y) -> (f z x) = (f z y).
+Proof.
+  smt.
+Qed.
+
+Goal forall (P:Z -> Z -> bool) x y z,
+  (Z.eqb x y) --> ((P z x) --> (P z y)).
+Proof.
+  smt.
+Qed.
+
+
+End PR.
+
+
+Section A_BV_EUF_LIA_PR.
+  Import BVList.BITVECTOR_LIST FArray.
+
+  Local Open Scope farray_scope.
+  Local Open Scope bv_scope. 
+
+  (* TODO *)
+  (* Goal forall (bv1 bv2 : bitvector 4) *)
+  (*        (a b c d : farray (bitvector 4) Z), *)
+  (*     bv1 = #b|0|0|0|0|  -> *)
+  (*     bv2 = #b|1|0|0|0|  -> *)
+  (*     c = b[bv1 <- 4]  -> *)
+  (*     d = b[bv1 <- 4][bv2 <- 4]  -> *)
+  (*     a = d[bv2 <- b[bv2]]  -> *)
+  (*     a = c. *)
+  (* Proof. *)
+  (*   smt. *)
+  (* Qed. *)
+
+  (* TODO *)
+  (* Goal forall (bv1 bv2 : bitvector 4) *)
+  (*        (a b c d : farray (bitvector 4) Z), *)
+  (*     bv1 = #b|0|0|0|0|  /\ *)
+  (*     bv2 = #b|1|0|0|0|  /\ *)
+  (*     c = b[bv1 <- 4]  /\ *)
+  (*     d = b[bv1 <- 4][bv2 <- 4]  /\ *)
+  (*     a = d[bv2 <- b[bv2]]  -> *)
+  (*     a = c. *)
+  (* Proof. *)
+  (*   smt. *)
+  (* Qed. *)
+
+  (** the example in the CAV paper *)
+  Goal forall (a b: farray Z Z) (v w x y: Z)
+              (r s: bitvector 4)
+              (f: Z -> Z)
+              (g: farray Z Z -> Z)
+              (h: bitvector 4 -> Z),
+              a[x <- v] = b /\ a[y <- w] = b ->
+              r = s /\ h r = v /\ h s = y ->
+              v < x + 1 /\ v > x - 1 ->
+              f (h r) = f (h s) \/ g a = g b.
+  Proof.
+    smt. (** "cvc4. verit." also solves the goal *)
+  Qed.
+
+  (** the example in the FroCoS paper *)
+  Goal forall (a b: farray Z Z) (v w x y z t: Z)
+              (r s: bitvector 4)
+              (f: Z -> Z)
+              (g: farray Z Z -> Z)
+              (h: bitvector 4 -> Z),
+              a[x <- v] = b /\ a[y <- w] = b ->
+              a[z <- w] = b /\ a[t <- v] = b ->
+              r = s -> v < x + 10 /\ v > x - 5 ->
+              ~ (g a = g b) \/ f (h r) = f (h s).
+  Proof.
+    smt. (** "cvc4. verit." also solves the goal *)
+  Qed.
+
+
+  Goal forall (a b: farray (bitvector 4) Z)
+         (x y: bitvector 4)
+         (v: Z),
+      b[bv_add y x <- v] = a /\
+      b = a[bv_add x y <- v]  ->
+      a = b.
+  Proof.
+    smt.
+    (* CVC4 preprocessing hole on BV *)
+    replace (bv_add x y) with (bv_add y x)
+      by apply bv_eq_reflect, bv_add_comm.
+    verit.
+  Qed.
+
+  Goal forall (a:farray Z Z), a = a.
+  Proof.
+    smt.
+  Qed.
+
+  (* TODO: will be ok when symmetry of equality is back for verit *)
+  (* Goal forall (a b: farray Z Z), a = b <->  b = a. *)
+  (* Proof.  *)
+  (*   smt. *)
+  (* Qed. *)
+
+End A_BV_EUF_LIA_PR.
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index ba69110..cfb8f16 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -1,3 +1,15 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
 Add Rec LoadPath "../src" as SMTCoq.
 
 Require Import SMTCoq.
@@ -34,8 +46,14 @@ Lemma fun_const2 :
     (forall x, g (f x) 2) -> g (f 3) 2.
 Proof.
   intros f g Hf.
-  verit_base Hf; vauto.
+  verit_bool_base Hf; vauto.
 Qed.
+(*
+Toplevel input, characters 916-942:
+ Warning: Bytecode compiler failed, falling back to standard conversion
+ [bytecode-compiler-failed,bytecode-compiler]
+*)
+
 
 (* veriT vernacular commands *)
 
@@ -143,9 +161,12 @@ Section Checker_Lia3.
   Verit_Checker "lia3.smt2" "lia3.vtlog".
 End Checker_Lia3.
 
+(* TODO: it does not go through anymore
+   Anomaly: File "trace/smtCommands.ml", line 102, characters 12-18: Assertion failed.
 Section Checker_Lia4.
   Verit_Checker "lia4.smt2" "lia4.vtlog".
 End Checker_Lia4.
+*)
 
 Section Checker_Lia5.
   Verit_Checker "lia5.smt2" "lia5.vtlog".
@@ -180,6 +201,14 @@ Section Checker_Lia5_holes.
 End Checker_Lia5_holes.
 *)
 
+Section Checker_Bv1.
+  Verit_Checker "bv1.smt2" "bv1.log".
+End Checker_Bv1.
+
+Section Checker_Bv2.
+  Verit_Checker "bv2.smt2" "bv2.log".
+End Checker_Bv2.
+
 
 Section Sat0.
   Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog".
@@ -301,10 +330,12 @@ Section Lia3.
   Compute @Euf_Checker.checker t_i_lia3 t_func_lia3 t_atom_lia3 t_form_lia3 root_lia3 used_roots_lia3 trace_lia3.
 End Lia3.
 
+(* TODO: it does not go through anymore
 Section Lia4.
   Parse_certif_verit t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4 "lia4.smt2" "lia4.vtlog".
   Compute @Euf_Checker.checker t_i_lia4 t_func_lia4 t_atom_lia4 t_form_lia4 root_lia4 used_roots_lia4 trace_lia4.
 End Lia4.
+*)
 
 Section Lia5.
   Parse_certif_verit t_i_lia5 t_func_lia5 t_atom_lia5 t_form_lia5 root_lia5 used_roots_lia5 trace_lia5 "lia5.smt2" "lia5.vtlog".
@@ -346,6 +377,16 @@ Section Lia5_holes.
 End Lia5_holes.
 *)
 
+Section Bv1.
+  Parse_certif_verit t_i_bv1 t_func_bv1 t_atom_bv1 t_form_bv1 root_bv1 used_roots_bv1 trace_bv1 "bv1.smt2" "bv1.log".
+  Compute @Euf_Checker.checker t_i_bv1 t_func_bv1 t_atom_bv1 t_form_bv1 root_bv1 used_roots_bv1 trace_bv1.
+End Bv1.
+
+Section Bv2.
+  Parse_certif_verit t_i_bv2 t_func_bv2 t_atom_bv2 t_form_bv2 root_bv2 used_roots_bv2 trace_bv2 "bv2.smt2" "bv2.log".
+  Compute @Euf_Checker.checker t_i_bv2 t_func_bv2 t_atom_bv2 t_form_bv2 root_bv2 used_roots_bv2 trace_bv2.
+End Bv2.
+
 
 Section Theorem_Sat0.
   Time Verit_Theorem theorem_sat0 "sat0.smt2" "sat0.vtlog".
@@ -443,9 +484,11 @@ Section Theorem_Lia3.
   Time Verit_Theorem theorem_lia3 "lia3.smt2" "lia3.vtlog".
 End Theorem_Lia3.
 
+(* TODO: it does not go through anymore
 Section Theorem_Lia4.
   Time Verit_Theorem theorem_lia4 "lia4.smt2" "lia4.vtlog".
 End Theorem_Lia4.
+*)
 
 Section Theorem_Lia5.
   Time Verit_Theorem theorem_lia5 "lia5.smt2" "lia5.vtlog".
@@ -482,6 +525,14 @@ End Theorem_Lia5_holes.
 Check theorem_lia5_holes.
 *)
 
+Section Theorem_Bv1.
+  Time Verit_Theorem theorem_bv1 "bv1.smt2" "bv1.log".
+End Theorem_Bv1.
+
+Section Theorem_Bv2.
+  Time Verit_Theorem theorem_bv2 "bv2.smt2" "bv2.log".
+End Theorem_Bv2.
+
 
 (* verit tactic *)
 
@@ -939,18 +990,20 @@ Proof.
   verit.
 Qed.
 
+(* TODO: fails with native-coq: "compilation error"
 Goal forall (i j:int),
     (i == j) && (negb (i == j)) = false.
 Proof.
   verit.
-  econstructor; eexact Int63Properties.reflect_eqb.
+  exact int63_compdec.
 Qed.
 
 Goal forall i j, (i == j) || (negb (i == j)).
 Proof.
   verit.
-  econstructor; eexact Int63Properties.reflect_eqb.
+  exact int63_compdec.
 Qed.
+*)
 
 
 (* Congruence in which some premises are REFL *)
@@ -968,103 +1021,100 @@ Proof.
 Qed.
 
 
-(*
-   Local Variables:
-   coq-load-path: ((rec "../src" "SMTCoq"))
-   End:
-*)
-
-(* Some examples of using verit with lemmas. Use <verit_base H1 .. Hn; vauto>
+(* Some examples of using verit with lemmas. Use <verit_bool_base H1 .. Hn; vauto>
    to temporarily add the lemmas H1 .. Hn to the verit environment. *)
 
 Lemma taut1 :
   forall f, f 2 =? 0 -> f 2 =? 0.
-Proof. intros f p. verit_base p; vauto. Qed.
+Proof. intros f p. verit_bool_base p; vauto. Qed.
 
 Lemma taut2 :
   forall f, 0 =? f 2 -> 0 =?f 2.
-Proof. intros f p. verit_base p; vauto. Qed.
+Proof. intros f p. verit_bool_base p; vauto. Qed.
 
 Lemma taut3 :
   forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0.
-Proof. intros f p1 p2. verit_base p1 p2; vauto. Qed.
+Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed.
 
 Lemma taut4 :
   forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0.
-Proof. intros f p1 p2. verit_base p1 p2; vauto. Qed.
+Proof. intros f p1 p2. verit_bool_base p1 p2; vauto. Qed.
+
+(* Lemma test_eq_sym a b : implb (a =? b) (b =? a). *)
+(* Proof. verit. *)
 
-Lemma taut5 :
-  forall f, 0 =? f 2 -> f 2 =? 0.
-Proof. intros f p. verit_base p; vauto. Qed.
+(* Lemma taut5 : *)
+(*   forall f, 0 =? f 2 -> f 2 =? 0. *)
+(* Proof. intros f p. verit_bool_base p; vauto. Qed. *)
 
 Lemma fun_const_Z :
   forall f , (forall x, f x =? 2) ->
              f 3 =? 2.
-Proof. intros f Hf. verit_base Hf; vauto. Qed.
+Proof. intros f Hf. verit_bool_base Hf; vauto. Qed.
 
 Lemma lid (A : bool) :  A -> A.
-Proof. intro a. verit_base a; vauto. Qed.
+Proof. intro a. verit_bool_base a; vauto. Qed.
 
 Lemma lpartial_id A :
   (xorb A A) -> (xorb A A).
-Proof. intro xa. verit_base xa; vauto. Qed.
+Proof. intro xa. verit_bool_base xa; vauto. Qed.
 
 Lemma llia1 X Y Z:
   (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) ->
   (X + Y <=? 10) || (X + Z <=? 12).
-Proof. intro p. verit_base p; vauto. Qed.
+Proof. intro p. verit_bool_base p; vauto. Qed.
 
 Lemma llia2 X:
   X - 3 =? 7 -> X >=? 10.
-Proof. intro p. verit_base p; vauto. Qed.
+Proof. intro p. verit_bool_base p; vauto. Qed.
 
 Lemma llia3 X Y:
   X >? Y -> Y + 1 <=? X.
-Proof. intro p. verit_base p; vauto. Qed.
+Proof. intro p. verit_bool_base p; vauto. Qed.
 
 Lemma llia6 X:
   andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10.
-Proof. intro p. verit_base p; vauto. Qed.
+Proof. intro p. verit_bool_base p; vauto. Qed.
 
 Lemma even_odd b1 b2 x1 x2:
   (ifb b1
        (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2))
        (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) ->
   ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)).
-Proof. intro p. verit_base p; vauto. Qed.
+Proof. intro p. verit_bool_base p; vauto. Qed.
 
 Lemma lcongr1 (a b : Z) (P : Z -> bool) f:
   (f a =? b) -> (P (f a)) -> P b.
-Proof. intros eqfab pfa. verit_base eqfab pfa; vauto. Qed.
+Proof. intros eqfab pfa. verit_bool_base eqfab pfa; vauto. Qed.
 
 Lemma lcongr2 (f:Z -> Z -> Z) x y z:
   x =? y -> f z x =? f z y.
-Proof. intro p. verit_base p; vauto. Qed.
+Proof. intro p. verit_bool_base p; vauto. Qed.
 
 Lemma lcongr3 (P:Z -> Z -> bool) x y z:
   x =? y -> P z x -> P z y.
-Proof. intros eqxy pzx. verit_base eqxy pzx; vauto. Qed.
+Proof. intros eqxy pzx. verit_bool_base eqxy pzx; vauto. Qed.
 
 Lemma test20 :  forall x, (forall a, a <? x) -> 0 <=? x = false.
-Proof. intros x H. verit_base H; vauto. Qed.
+Proof. intros x H. verit_bool_base H; vauto. Qed.
 
 Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
-Proof. intros x H. verit_base H; vauto. Qed.
+Proof. intros x H. verit_bool_base H; vauto. Qed.
 
-Lemma un_menteur (a b c d : Z) dit:
-  dit a =? c ->
-  dit b =? d ->
-  (d =? a) || (b =? c) ->
-  (a =? c) || (a =? d) ->
-  (b =? c) || (b =? d) ->
-  a =? d.
-Proof. intros H1 H2 H3 H4 H5. verit_base H1 H2 H3 H4 H5; vauto. Qed.
+(* Lemma un_menteur (a b c d : Z) dit: *)
+(*   dit a =? c -> *)
+(*   dit b =? d -> *)
+(*   (d =? a) || (b =? c) -> *)
+(*   (a =? c) || (a =? d) -> *)
+(*   (b =? c) || (b =? d) -> *)
+(*   a =? d. *)
+(* Proof. intros H1 H2 H3 H4 H5. verit_bool_base H1 H2 H3 H4 H5; vauto. Qed. *)
 
 Lemma const_fun_is_eq_val_0 :
   forall f : Z -> Z,
     (forall a b, f a =? f b) ->
     forall x, f x =? f 0.
-Proof. intros f Hf. verit_base Hf; vauto. Qed.
+Proof. intros f Hf. verit_bool_base Hf; vauto. Qed.
 
 (* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to
    the environment. If you did so in a section then, at the end of the section,
@@ -1143,7 +1193,7 @@ End mult3.
 (*   Hypothesis mult_Sx : forall x y, mult (x+1) y =? mult x y + y. *)
 
 (*   Lemma mult_1_x : forall x, mult 1 x =? x. *)
-(*   Proof. verit_base mult_0 mult_Sx. *)
+(*   Proof. verit_bool_base mult_0 mult_Sx. *)
 (*   Qed. *)
 (* End mult. *)
 
@@ -1163,8 +1213,7 @@ End implicit_transform.
 
 Section list.
   Variable Zlist : Type.
-  Hypothesis dec_Zlist :
-    {eq : Zlist -> Zlist -> bool & forall x y : Zlist, reflect (x = y) (eq x y)}.
+  Hypothesis dec_Zlist : CompDec Zlist.
   Variable nil : Zlist.
   Variable cons : Z -> Zlist -> Zlist.
   Variable inlist : Z -> Zlist -> bool.
@@ -1276,15 +1325,15 @@ Section group.
 
   Lemma unique_identity e':
     (forall z, op e' z =? z) -> e' =? e.
-  Proof. intros pe'. verit_base pe'; vauto. Qed.
+  Proof. intros pe'. verit_bool_base pe'; vauto. Qed.
 
   Lemma simplification_right x1 x2 y:
       op x1 y =? op x2 y -> x1 =? x2.
-  Proof. intro H. verit_base H; vauto. Qed.
+  Proof. intro H. verit_bool_base H; vauto. Qed.
 
   Lemma simplification_left x1 x2 y:
       op y x1 =? op y x2 -> x1 =? x2.
-  Proof. intro H. verit_base H; vauto. Qed.
+  Proof. intro H. verit_bool_base H; vauto. Qed.
 
   Clear_lemmas.
 End group.
diff --git a/unit-tests/Tests_zchaff.v b/unit-tests/Tests_zchaff.v
index 28251f8..87d6db2 100644
--- a/unit-tests/Tests_zchaff.v
+++ b/unit-tests/Tests_zchaff.v
@@ -1,3 +1,15 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
 Add Rec LoadPath "../src" as SMTCoq.
 
 Require Import SMTCoq.
diff --git a/unit-tests/bv1.log b/unit-tests/bv1.log
new file mode 100644
index 0000000..fc101e2
--- /dev/null
+++ b/unit-tests/bv1.log
@@ -0,0 +1,12 @@
+1:(input ((not #1:(= a a))))
+2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a)])))
+3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8)))) 2 2)
+4:(equiv2 (#1 (not #4)) 3)
+5:(resolution ((not #4)) 1 4)
+6:(not_and ((not #5) (not #6)) 5)
+7:(equiv_neg1 (#5 (not #7)))
+8:(equiv_neg2 (#5 #7))
+9:(resolution ((not #6)) 7 8 6)
+10:(equiv_neg1 (#6 (not #8)))
+11:(equiv_neg2 (#6 #8))
+12:(resolution () 10 11 9)
diff --git a/unit-tests/bv1.smt2 b/unit-tests/bv1.smt2
new file mode 100644
index 0000000..c23b151
--- /dev/null
+++ b/unit-tests/bv1.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 2))
+(assert (not (= a a)))
+(check-sat)
+(exit)
diff --git a/unit-tests/bv2.log b/unit-tests/bv2.log
new file mode 100644
index 0000000..5bcd227
--- /dev/null
+++ b/unit-tests/bv2.log
@@ -0,0 +1,15 @@
+1:(input ((not #1:(= a a))))
+2:(bbvar (#2:(bbT a [#7:(bitof 0 a) #8:(bitof 1 a) #9:(bitof 2 a)])))
+3:(bbeq (#3:(= #1 #4:(and #5:(= #7 #7) #6:(= #8 #8) #10:(= #9 #9)))) 2 2)
+4:(equiv2 (#1 (not #4)) 3)
+5:(resolution ((not #4)) 1 4)
+6:(not_and ((not #5) (not #6) (not #10)) 5)
+7:(equiv_neg1 (#5 (not #7)))
+8:(equiv_neg2 (#5 #7))
+9:(resolution ((not #6) (not #10)) 7 8 6)
+10:(equiv_neg1 (#6 (not #8)))
+11:(equiv_neg2 (#6 #8))
+12:(resolution ((not #10)) 10 11 9)
+13:(equiv_neg1 (#10 (not #9)))
+14:(equiv_neg2 (#10 #9))
+15:(resolution () 13 14 12)
diff --git a/unit-tests/bv2.smt2 b/unit-tests/bv2.smt2
new file mode 100644
index 0000000..49156c7
--- /dev/null
+++ b/unit-tests/bv2.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 3))
+(assert (not (= a a)))
+(check-sat)
+(exit)
diff --git a/unit-tests/demo_lfsc_bool.v b/unit-tests/demo_lfsc_bool.v
new file mode 100644
index 0000000..d89954f
--- /dev/null
+++ b/unit-tests/demo_lfsc_bool.v
@@ -0,0 +1,199 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import SMTCoq.
+Require Import Bool PArray Int63 List ZArith BVList Logic.
+Import ListNotations.
+Local Open Scope list_scope.
+Local Open Scope int63_scope.
+Local Open Scope Z_scope.
+Local Open Scope bv_scope.
+
+
+Infix "-->" := implb (at level 60, right associativity) : bool_scope.
+
+
+Import BVList.BITVECTOR_LIST. 
+Require Import FArray.
+
+Section BV.
+
+  Import BVList.BITVECTOR_LIST.
+
+  Local Open Scope bv_scope.
+
+  Goal forall (bv1 bv2 bv3 bv4: bitvector 4),
+      bv_eq #b|0|0|0|0| bv1 &&
+      bv_eq #b|1|0|0|0| bv2 &&
+      bv_eq #b|1|1|0|0| bv3 -->
+      bv_eq #b|1|1|1|0| bv4 -->
+      bv_ult bv1 bv2  || bv_ult bv3 bv1 --> bv_ult bv1 bv3 --> bv_ult bv1 bv4 || bv_ult bv4 bv1.
+  Proof.
+     smt.
+  Qed.
+
+  Goal forall (a: bitvector 32), bv_eq a a.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (bv1 bv2: bitvector 4),
+       (Bool.eqb (bv_eq bv1 bv2) (bv_eq bv2 bv1)).
+  Proof.
+     smt.
+  Qed.
+
+  Goal forall (bv1 bv2 bv3 bv4: bitvector 4),
+      bv_eq #b|0|0|0|0| bv1 &&
+      bv_eq #b|1|0|0|0| bv2 &&
+      bv_eq #b|1|1|0|0| bv3 -->
+      bv_eq #b|1|1|1|0| bv4 -->
+      bv_ult bv1 bv2 || bv_ult bv3 bv1 && bv_ult bv3 bv4.
+  Proof.
+     smt.
+  Qed.
+
+  Goal forall (a b c: bitvector 4),
+                                 (bv_eq c (bv_and a b))  -->
+                                 (bv_eq (bv_and (bv_and c a) b) c).
+  Proof.
+     smt.
+  Qed.
+
+End BV.
+
+Section Arrays.
+  Import BVList.BITVECTOR_LIST.
+  Import FArray.
+
+  Local Open Scope farray_scope.
+  Local Open Scope bv_scope.
+
+  Goal forall (a:farray Z Z), equal a a.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: farray Z Z), Bool.eqb (equal a b) (equal b a).
+  Proof. 
+    smt.
+  Qed.
+
+  Goal forall (a b: farray (bitvector 8) (bitvector 8)), Bool.eqb (equal a b) (equal b a).
+  Proof. 
+    smt.
+  Qed.
+
+  Goal forall (a b c d: farray Z Z),
+      equal b[0 <- 4] c -->
+      equal d b[0 <- 4][1 <- 4]  &&
+      equal a d[1 <- b[1]]  -->
+      equal a c.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (bv1 bv2 : bitvector 4)
+         (a b c d : farray (bitvector 4) Z),
+      bv_eq #b|0|0|0|0| bv1  -->
+      bv_eq #b|1|0|0|0| bv2  -->
+      equal c b[bv1 <- 4] -->
+      equal d b[bv1 <- 4][bv2 <- 4] -->
+      equal a d[bv2 <- b[bv2]] -->
+      equal a c.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: farray Z Z)
+         (v w x y: Z)
+         (g: farray Z Z -> Z)
+         (f: Z -> Z),
+         (equal a[x <- v] b) && (equal a[y <- w] b) --> (Z.eqb (f x) (f y)) || (Z.eqb (g a) (g b)).
+  Proof.
+    smt.
+  Qed.
+
+Goal forall (a b: farray Z Z) i,
+      Z.eqb (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) 4.
+Proof.
+    smt.
+    rewrite read_over_other_write; try easy.
+    rewrite read_over_same_write; try easy; try apply Z_compdec.
+    rewrite read_over_same_write; try easy; try apply Z_compdec.
+Qed.
+
+End Arrays.
+
+Section UF.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         Z.eqb y x --> Z.eqb (f x) (f y).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         Z.eqb (f x) (f y) --> Z.eqb (f y) (f x).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         Z.eqb (x + 1)  (y + 1) --> Z.eqb (f y) (f x).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         Z.eqb x (y + 1) --> Z.eqb (f y) (f (x - 1)).
+  Proof.
+    smt.
+  Qed.
+
+
+Goal forall (f:Z -> Z -> Z) x y z, (Z.eqb x y) --> Z.eqb (f z x) (f z y).
+Proof.
+  smt.
+Qed.
+
+End UF.
+
+
+Section LIA.
+
+  Goal forall (a b: Z), Bool.eqb (Z.eqb a b)  (Z.eqb b a).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: Z), (Z.eqb a a) && (Z.eqb b b).
+  Proof.
+    smt.
+  Qed.
+
+
+End LIA.
+
+
+
+
+
+
diff --git a/unit-tests/demo_lfsc_prop.v b/unit-tests/demo_lfsc_prop.v
new file mode 100644
index 0000000..00acfef
--- /dev/null
+++ b/unit-tests/demo_lfsc_prop.v
@@ -0,0 +1,233 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2019                                          *)
+(*                                                                        *)
+(*     See file "AUTHORS" for the list of authors                         *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Require Import SMTCoq.
+Require Import Bool PArray Int63 List ZArith BVList Logic.
+Import ListNotations.
+Local Open Scope list_scope.
+Local Open Scope int63_scope.
+Local Open Scope Z_scope.
+Local Open Scope bv_scope.
+
+Import BVList.BITVECTOR_LIST. 
+Require Import FArray.
+
+
+Section BV.
+
+  Import BVList.BITVECTOR_LIST.
+
+  Local Open Scope bv_scope.
+
+  (*
+  (** cvc4 preprocesses the entire goal *)
+  Goal forall (a b c: bitvector 4), 
+      bv_mult a (bv_add b c) = bv_add (bv_mult a b) (bv_mult a c).
+  *)
+
+
+  Goal forall (a b: bitvector 8), 
+      #b|1|0|0|0|0|0|0|0| = a ->
+      #b|1|0|0|0|0|0|0|0| = b -> (bv_mult a b) =  #b|0|0|0|0|0|0|0|0|.
+  Proof.
+     smt.
+  Qed.
+
+(*
+
+Goal forall (a b: bitvector 32), a = b.
+Proof. smt. Fail Qed.
+
+*)
+
+
+  Goal forall (bv1 bv2 bv3 bv4: bitvector 4),
+      #b|0|0|0|0| = bv1 /\
+      #b|1|0|0|0| = bv2 /\
+      #b|1|1|0|0| = bv3 ->
+      #b|1|1|1|0| = bv4 ->
+      bv_ultP bv1 bv2  \/ bv_ultP bv3 bv1 -> bv_ultP bv1 bv3 -> bv_ultP bv1 bv4 \/ bv_ultP bv4 bv1.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a: bitvector 32), a = a.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (bv1 bv2: bitvector 4),
+       bv1 = bv2 <-> bv2 = bv1.
+  Proof.
+     smt.
+  Qed.
+
+  Goal forall (bv1 bv2 bv3 bv4: bitvector 4),
+      bv1 = #b|0|0|0|0| /\
+      bv2 = #b|1|0|0|0| /\
+      bv3 = #b|1|1|0|0| ->
+      bv4 = #b|1|1|1|0| ->
+      bv_ultP bv1 bv2 \/ bv_ultP bv3 bv1 /\ bv_ultP bv3 bv4.
+  Proof.
+     smt.
+  Qed.
+
+  Goal forall (a b c: bitvector 4),
+                                 (c = (bv_and a b)) ->
+                                 ((bv_and (bv_and c a) b) = c).
+  Proof.
+     smt.
+  Qed.
+
+
+
+End BV.
+
+Section Arrays.
+  Import BVList.BITVECTOR_LIST.
+  Import FArray.
+
+  Local Open Scope farray_scope.
+  Local Open Scope bv_scope.
+
+  Goal forall (a:farray Z Z), a = a.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: farray Z Z), a = b <->  b = a.
+  Proof. 
+    smt.
+  Qed.
+
+  Goal forall (a b: farray (bitvector 8) (bitvector 8)), a = b <->  b = a.
+  Proof. 
+    smt.
+  Qed.
+
+  Goal forall (a b c d: farray Z Z),
+      b[0 <- 4] = c ->
+      d = b[0 <- 4][1 <- 4]  /\
+      a = d[1 <- b[1]]  ->
+      a = c.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (bv1 bv2 : bitvector 4)
+         (a b c d : farray (bitvector 4) Z),
+      bv1 = #b|0|0|0|0|  ->
+      bv2 = #b|1|0|0|0|  ->
+      c = b[bv1 <- 4]  ->
+      d = b[bv1 <- 4][bv2 <- 4]  ->
+      a = d[bv2 <- b[bv2]]  ->
+      a = c.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: farray Z Z)
+         (v w x y: Z)
+         (g: farray Z Z -> Z)
+         (f: Z -> Z),
+         (a[x <- v] = b) /\ a[y <- w] = b  ->
+         (f x) = (f y) \/  (g a) = (g b).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: farray Z Z) i,
+      a[i <- 3][1 <- b[i <- 4][i]][2 <- 2][1] = 4.
+  Proof.
+    smt.
+    rewrite read_over_other_write; [ | easy].
+    rewrite read_over_write.
+    rewrite read_over_write; auto.
+Qed.
+
+End Arrays.
+
+Section UF.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         y = x -> (f x) = (f y).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         (f x) = (f y) -> (f y) = (f x).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         x + 1 = (y + 1) -> (f y) = (f x).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall
+         (x y: Z)
+         (f: Z -> Z),
+         x = (y + 1) -> (f y) = (f (x - 1)).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (f:Z -> Z -> Z) x y z, (x = y) -> (f z x) = (f z y).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (t: Type) (p: CompDec t) (x y: t), (x = y) <-> (x = y).
+  Proof.
+    smt.
+  Qed.
+
+End UF.
+
+
+Section LIA.
+
+   Goal forall a b, a < b -> a < (b + 10).
+   Proof. 
+     smt.
+   Qed.
+
+  Goal forall (a b: Z), a = b <-> b = a.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: Z), a = a /\ b = b.
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: Z), a < b -> a < (b + 1).
+  Proof.
+    smt.
+  Qed.
+
+  Goal forall (a b: Z), (a < b) -> (a + 2 < b + 3).
+  Proof.
+    smt.
+  Qed.
+
+End LIA.
diff --git a/unit-tests/ex1.lfsc b/unit-tests/ex1.lfsc
new file mode 100644
index 0000000..d96c5be
--- /dev/null
+++ b/unit-tests/ex1.lfsc
@@ -0,0 +1,23 @@
+unsat
+(check
+ ;; Declarations
+(% a (term Bool)
+(% b (term Bool)
+(% c (term Bool)
+(% A1 (th_holds (not (impl (and (impl (p_app a) (p_app b)) (impl (p_app b) (p_app c))) (impl (p_app a) (p_app c)))))
+ ;; Proof of empty clause follows
+(: (holds cln)
+ ;; Preprocessing 
+ ;; Clauses
+(decl_atom (p_app b) (\ var3 (\ atom3
+(decl_atom (p_app a) (\ var2 (\ atom2
+(satlem _ _ (asf _ _ _ atom3 (\ lit6 (ast _ _ _ atom2 (\ lit5 (clausify_false (contra _ (or_elim_1 _ _ (not_not_intro _ lit5) (impl_elim _ _ (and_elim_1 _ _ (and_elim_1 _ _ (not_impl_elim _ _ A1))))) lit6)))))) (\ pb2
+(decl_atom (p_app c) (\ var4 (\ atom4
+(satlem _ _ (asf _ _ _ atom4 (\ lit8 (ast _ _ _ atom3 (\ lit7 (clausify_false (contra _ (or_elim_1 _ _ (not_not_intro _ lit7) (impl_elim _ _ (and_elim_2 _ _ (and_elim_1 _ _ (not_impl_elim _ _ A1))))) lit8)))))) (\ pb3
+(satlem _ _ (asf _ _ _ atom2 (\ lit4 (clausify_false (contra _ (and_elim_1 _ _ (not_impl_elim _ _ (and_elim_2 _ _ (not_impl_elim _ _ A1)))) lit4)))) (\ pb4
+(satlem _ _ (ast _ _ _ atom4 (\ lit9 (clausify_false (contra _ lit9 (and_elim_2 _ _ (not_impl_elim _ _ (and_elim_2 _ _ (not_impl_elim _ _ A1)))))))) (\ pb5
+ ;; Theory Lemmas
+(satlem_simplify _ _ _ (Q _ _ pb2 pb4 var2) (\cl6
+(satlem_simplify _ _ _ (Q _ _ pb3 cl6 var3) (\cl7
+(satlem_simplify _ _ _ (Q _ _ pb5 cl7 var4) (\empty empty)))))))))))))))))))))))))))))
+;;
diff --git a/unit-tests/ex1.smt2 b/unit-tests/ex1.smt2
new file mode 100644
index 0000000..51685ed
--- /dev/null
+++ b/unit-tests/ex1.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_SAT)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+
+(assert (not (=> (and (=> a b) (=> b c)) (=> a c))))
+
+(check-sat)
+
+(exit)
+
diff --git a/unit-tests/large1.v b/unit-tests/large1.v
new file mode 100644
index 0000000..ee3ef55
--- /dev/null
+++ b/unit-tests/large1.v
@@ -0,0 +1,88 @@
+Require Import SMTCoq.
+
+(* For Notations *)
+Import Bool PArray Int63 List ZArith FArray BVList.BITVECTOR_LIST.
+Import ListNotations.
+Open Scope list_scope.
+Open Scope farray_scope.
+Open Scope bv_scope.
+
+Infix "-->" := implb (at level 60, right associativity) : bool_scope.
+Notation "¬ x" := (negb x) (at level 30, right associativity): bool_scope.
+
+
+
+Goal forall
+    (a1 : (farray Z Z))
+    ( e1 : Z)
+    ( e10 : Z)
+    ( e2 : Z)
+    ( e3 : Z)
+    ( e4 : Z)
+    ( e5 : Z)
+    ( e6 : Z)
+    ( e7 : Z)
+    ( e8 : Z)
+    ( e9 : Z)
+    ( i1 : Z)
+    ( i10 : Z)
+    ( i2 : Z)
+    ( i3 : Z)
+    ( i4 : Z)
+    ( i5 : Z)
+    ( i6 : Z)
+    ( i7 : Z)
+    ( i8 : Z)
+    ( i9 : Z)
+    (sk : (farray Z Z) -> (farray Z Z) -> Z),
+    
+    negb (i9 =? i10) &&
+    negb (i8 =? i10) &&
+    negb (i8 =? i9) &&
+    negb (i7 =? i10) &&
+    negb (i7 =? i9) &&
+    negb (i7 =? i8) &&
+    negb (i6 =? i10) &&
+    negb (i6 =? i9) &&
+    negb (i6 =? i8) &&
+    negb (i6 =? i7) &&
+    negb (i5 =? i10) &&
+    negb (i5 =? i9) &&
+    negb (i5 =? i8) &&
+    negb (i5 =? i7) &&
+    negb (i5 =? i6) &&
+    negb (i4 =? i10) &&
+    negb (i4 =? i9) &&
+    negb (i4 =? i8) &&
+    negb (i4 =? i7) &&
+    negb (i4 =? i6) &&
+    negb (i4 =? i5) &&
+    negb (i3 =? i10) &&
+    negb (i3 =? i9) &&
+    negb (i3 =? i8) &&
+    negb (i3 =? i7) &&
+    negb (i3 =? i6) &&
+    negb (i3 =? i5) &&
+    negb (i3 =? i4) &&
+    negb (i2 =? i10) &&
+    negb (i2 =? i9) &&
+    negb (i2 =? i8) &&
+    negb (i2 =? i7) &&
+    negb (i2 =? i6) &&
+    negb (i2 =? i5) &&
+    negb (i2 =? i4) &&
+    negb (i2 =? i3) &&
+    negb (i1 =? i10) &&
+    negb (i1 =? i9) &&
+    negb (i1 =? i8) &&
+    negb (i1 =? i7) &&
+    negb (i1 =? i6) &&
+    negb (i1 =? i5) &&
+    negb (i1 =? i4) &&
+    negb (i1 =? i3) &&
+    negb (i1 =? i2) -->
+
+    ((select (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) (sk (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) (store (store (store (store (store (store (store (store (store (store a1 i9 e9) i3 e3) i5 e5) i4 e4) i6 e6) i1 e1) i10 e10) i2 e2) i8 e8) i7 e7))) =? (select (store (store (store (store (store (store (store (store (store (store a1 i9 e9) i3 e3) i5 e5) i4 e4) i6 e6) i1 e1) i10 e10) i2 e2) i8 e8) i7 e7) (sk (store (store (store (store (store (store (store (store (store (store a1 i1 e1) i2 e2) i3 e3) i4 e4) i5 e5) i6 e6) i7 e7) i8 e8) i9 e9) i10 e10) (store (store (store (store (store (store (store (store (store (store a1 i9 e9) i3 e3) i5 e5) i4 e4) i6 e6) i1 e1) i10 e10) i2 e2) i8 e8) i7 e7)))).
+Proof.
+  Time smt.
+Qed.
diff --git a/unit-tests/sat6.smt2 b/unit-tests/sat6.smt2
index acef584..3c73489 100644
--- a/unit-tests/sat6.smt2
+++ b/unit-tests/sat6.smt2
@@ -5,6 +5,6 @@
 (declare-fun d () Bool)
 (assert (and a b))
 (assert (or c d))
-(assert (not (or c (and a b d))))
+(assert (not (or c (and a (and b d)))))
 (check-sat)
 (exit)