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)