diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-07-20 16:01:00 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-07-20 16:01:00 +0200 |
| commit | c314187dac30be326b35eab9a6f4665523c2eac0 (patch) | |
| tree | 7c6ed7f89b7031c299359a4bb62dd93d99a2bd72 | |
| parent | c8a696682fcbdc720d67eb8d93f2c0c5b5c03548 (diff) | |
| download | smtcoq-c314187dac30be326b35eab9a6f4665523c2eac0.tar.gz smtcoq-c314187dac30be326b35eab9a6f4665523c2eac0.zip | |
Testing BV subtraction
| -rw-r--r-- | unit-tests/Tests_lfsc_tactics.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index 2268cb9..387ed21 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -706,6 +706,22 @@ Section A_BV_EUF_LIA_PR. smt. Qed. + + (* Testing bit-vectors substraction: this is a syntactic check that it + is correctly exported to SMT-LIB, CVC4-1.6 does not provide useful + proofs anyway. *) + + Goal forall (x: bitvector 1), bv_subt x #b|0| = x. + Proof using. + smt. + Admitted. + + (* The original issue (unvalid) *) + Goal forall (x: bitvector 1), bv_subt (bv_shl #b|0| x) #b|0| = #b|0|. + Proof using. + smt. + Admitted. + End A_BV_EUF_LIA_PR. |