+; EXPECT: unsat\r
+; COMMAND-LINE: --sygus-out=status\r
+(set-logic BV)\r
+\r
+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))\r
+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))\r
+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))\r
+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))\r
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))\r
+\r
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)\r
+(\r
+\r
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
+ (shl1 Start)\r
+ (shr1 Start)\r
+ (shr4 Start)\r
+ (shr16 Start)\r
+ (bvand Start Start)\r
+ (bvor Start Start)\r
+ (bvxor Start Start)\r
+ (bvadd Start Start)\r
+ (if0 Start Start Start)\r
+ ))\r
+)\r
+)\r
+\r
+\r
+(constraint (= (f #x9db91b67d1eee4b4) #x00009db91b67d1ee))\r
+(constraint (= (f #x211526232b50ea1d) #xdeead9dcd4af15e2))\r
+(constraint (= (f #xedcec1de604e94ec) #x0000edcec1de604e))\r
+(constraint (= (f #xede1841179ee3684) #x0000ede1841179ee))\r
+(constraint (= (f #x9c623bcc40d252bd) #x639dc433bf2dad42))\r
+(constraint (= (f #x4601c6d84a50d01b) #xb9fe3927b5af2fe4))\r
+(constraint (= (f #x0c5ed1e748c4e26c) #x00000c5ed1e748c4))\r
+(constraint (= (f #x6bb653229e60ee94) #x00006bb653229e60))\r
+(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))\r
+(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))\r
+\r
+(synth-fun g ( (x (BitVec 64))) (BitVec 64)\r
+(\r
+\r
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)\r
+ (shl1 Start)\r
+ (shr1 Start)\r
+ (shr4 Start)\r
+ (shr16 Start)\r
+ (bvand Start Start)\r
+ (bvor Start Start)\r
+ (bvxor Start Start)\r
+ (bvadd Start Start)\r
+ (if0 Start Start Start)\r
+ ))\r
+)\r
+)\r
+\r
+(constraint (= (g #xd5a6481ee2ba1030) #xfffffffffffffffe))\r
+(constraint (= (g #x03e887e72dee55cd) #x03e887e72dee55cd))\r
+(constraint (= (g #xaced92921c8e318d) #xaced92921c8e318d))\r
+(constraint (= (g #x95e5e4184e40aaec) #xfffffffffffffffe))\r
+(constraint (= (g #x352367e34d76550b) #x352367e34d76550b))\r
+(constraint (= (g #x398560eeee7b1b6c) #xfffffffffffffffe))\r
+(constraint (= (g #x099be4899986c29a) #xfffffffffffffffe))\r
+(constraint (= (g #xb14b75be2e13445a) #xfffffffffffffffe))\r
+(constraint (= (g #xb4c680ad7e6b16ce) #xfffffffffffffffe))\r
+(constraint (= (g #x7e4954872868acb8) #xfffffffffffffffe))\r
+(check-synth)\r