diff options
Diffstat (limited to 'unit-tests')
-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. |