Skip to content

Commit

Permalink
Changed smt file
Browse files Browse the repository at this point in the history
  • Loading branch information
oskari1 committed Sep 4, 2023
1 parent 2515287 commit d763489
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions smt-problems/small_forall_example_2.smt2
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(declare-const x (_ BitVec 64))
(declare-const y (_ BitVec 64))
(assert (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
(= (bvsub (bvadd x y) (bvshl (bvand x y) (_ bv1 64))) (bvxor x y))))
(declare-const z (_ BitVec 64))
(assert (forall ((x (_ BitVec 64)) (z (_ BitVec 64)))
(= (bvsub (bvadd x z) (bvshl (bvand x z) (_ bv1 64))) (bvxor x z))))

(check-sat)

0 comments on commit d763489

Please sign in to comment.