From d7634893bf2e3cc81f3c1bc39383b00ba2ef27ab Mon Sep 17 00:00:00 2001 From: ojyrkinen Date: Mon, 4 Sep 2023 11:50:13 +0200 Subject: [PATCH] Changed smt file --- smt-problems/small_forall_example_2.smt2 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/smt-problems/small_forall_example_2.smt2 b/smt-problems/small_forall_example_2.smt2 index 2d3efa7a..cb107b69 100644 --- a/smt-problems/small_forall_example_2.smt2 +++ b/smt-problems/small_forall_example_2.smt2 @@ -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)