diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-01 10:39:13 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-01 10:39:13 -0700 |
commit | 0cc88cf09c59effc41a076d4d78ef2082f780509 (patch) | |
tree | 29499ec78572f954eb053083a32ac4bfca4aa530 /proofs/signatures/ex_bv.plf | |
parent | 689f1f89ccea1825a7b222e5af97f5133069ff74 (diff) | |
parent | 172e0bd41cbd410fb1e66bc32a9a9b8523bc40e2 (diff) |
Diffstat (limited to 'proofs/signatures/ex_bv.plf')
-rw-r--r-- | proofs/signatures/ex_bv.plf | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/signatures/ex_bv.plf b/proofs/signatures/ex_bv.plf index 58494e793..332d7765c 100644 --- a/proofs/signatures/ex_bv.plf +++ b/proofs/signatures/ex_bv.plf @@ -24,9 +24,9 @@ (decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5 ; bitblasting formulas -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt1 bt2) (\ bf1 +(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt1 bt2) (\ bf1 (th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2 -(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt2 bt4) (\ bf3 +(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt2 bt4) (\ bf3 ; CNFication ; a.4 V ~b.4 @@ -44,7 +44,7 @@ trust ))) (\ C3 -; b.4 +; b.4 (satlem _ _ (asf _ _ _ a2 (\ l2 (clausify_false @@ -52,7 +52,7 @@ ))) (\ C6 -(satlem_simplify _ _ _ +(satlem_simplify _ _ _ (R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) ))))))))))))))))))))))))))))))))))))))))))))) |