diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-12 16:25:15 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-12 16:25:15 -0600 |
| commit | bc37e46f4861e0a3e753c1cfbbccda4630a49562 (patch) | |
| tree | 94f6f7a75bcfe92f5d7a63a4ebb40201426d1819 /test/regress/regress1/bv/issue3654.smt2 | |
| parent | 850ac17e46c97cab39122bfcd01dcbe459d1589a (diff) | |
| parent | f38cd31ddfd3d5caa2ffe3a0ffafbb2b0394391b (diff) | |
Merge branch 'master' into renameJavaPackagerenameJavaPackage
Diffstat (limited to 'test/regress/regress1/bv/issue3654.smt2')
| -rw-r--r-- | test/regress/regress1/bv/issue3654.smt2 | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress1/bv/issue3654.smt2 b/test/regress/regress1/bv/issue3654.smt2 new file mode 100644 index 000000000..59c11456f --- /dev/null +++ b/test/regress/regress1/bv/issue3654.smt2 @@ -0,0 +1,24 @@ +; COMMAND_LINE: --ext-rew-prep +; EXPECT: sat +(set-logic QF_BV) +(declare-fun a () (_ BitVec 4)) +(assert (let ((a!1 ((_ sign_extend 3) + (ite (bvult ((_ sign_extend 15) #b0) #x2b7e) #b1 #b0))) + (a!2 ((_ zero_extend 15) + (ite (distinct #x2b7e ((_ sign_extend 12) a)) #b1 #b0))) + (a!4 (bvsgt (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)) + ((_ zero_extend 12) a))) + (a!5 (bvugt (ite (bvult ((_ sign_extend 15) #b0) #x2b7e) #b1 #b0) #b0)) + (a!6 (bvugt (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)) + #x2b7e))) +(let ((a!3 (bvslt a!2 + (bvlshr (bvadd #x2b7e ((_ sign_extend 12) a)) + ((_ sign_extend 12) a)))) + (a!7 (xor (ite a!4 a!5 a!4) + a!6 + (= (bvxnor #x2b7e ((_ zero_extend 12) a)) + (bvadd #x2b7e ((_ sign_extend 12) a)))))) + (ite (bvule a!1 a) a!3 a!7)))) +(check-sat) |