diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-07-20 16:02:42 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-07-20 16:02:42 +0200 |
| commit | 2dea67ed5a22708e222936f66a1412ab15a0c72c (patch) | |
| tree | 9962dbccbded62fa4703ab77919514fd5ef25bcb | |
| parent | 862c8b445d4c8f1f83f435cb4d282b81c16ebb82 (diff) | |
| parent | c314187dac30be326b35eab9a6f4665523c2eac0 (diff) | |
| download | smtcoq-2dea67ed5a22708e222936f66a1412ab15a0c72c.tar.gz smtcoq-2dea67ed5a22708e222936f66a1412ab15a0c72c.zip | |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11
| -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. |