From c314187dac30be326b35eab9a6f4665523c2eac0 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 20 Jul 2020 16:01:00 +0200 Subject: Testing BV subtraction --- unit-tests/Tests_lfsc_tactics.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'unit-tests') 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. -- cgit