diff options
Diffstat (limited to 'test/regress/regress0/sygus/icfp_28_10.sy')
-rw-r--r-- | test/regress/regress0/sygus/icfp_28_10.sy | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy new file mode 100644 index 000000000..6e1610337 --- /dev/null +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -0,0 +1,40 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi + +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) + + +(constraint (= (f #xd74594057974e439) #x0000d74594057974)) +(constraint (= (f #x74641ebeee92e8a2) #x000074641ebeee92)) +(constraint (= (f #x91c80141d7ec76b1) #x000091c80141d7ec)) +(constraint (= (f #xe4e55862e5ee4bec) #x0000e4e55862e5ee)) +(constraint (= (f #x367da67ede4260ce) #x0000367da67ede42)) +(constraint (= (f #xa365eb36246b3d8e) #x0000a365eb36246b)) +(constraint (= (f #xcd8a44a6d4c09c29) #x0000cd8a44a6d4c0)) +(constraint (= (f #xa97e9b9b7970433d) #x0000a97e9b9b7970)) +(constraint (= (f #x474dec0dd75d6894) #x0000474dec0dd75d)) +(constraint (= (f #x12430014ed058b24) #x000012430014ed05)) +(check-synth) |