diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-07 15:31:08 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-07 15:31:08 +0000 |
| commit | fbaa1e2bdb2d10465b76fc6fc3fbfd3318612493 (patch) | |
| tree | aa4c17e44331f991c221705da92b28d6c02527f5 /test/regress/regress0/aufbv | |
| parent | 49dd14da8d872403b4d772a2d49224e4d6bda227 (diff) | |
Added small test case for diseq propagation
Diffstat (limited to 'test/regress/regress0/aufbv')
| -rw-r--r-- | test/regress/regress0/aufbv/diseqprop.01.smt | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/diseqprop.01.smt b/test/regress/regress0/aufbv/diseqprop.01.smt new file mode 100644 index 000000000..543684e21 --- /dev/null +++ b/test/regress/regress0/aufbv/diseqprop.01.smt @@ -0,0 +1,12 @@ +(benchmark B_ + :status unsat + :logic QF_AUFBV + :extrafuns ((v6 BitVec[32])) + :extrafuns ((v7 BitVec[32])) + :extrafuns ((a1 Array[32:8])) + :formula + (and +(not (= (store a1 v6 bv0[8]) (store a1 v6 (extract[7:0] v7)))) +(or (= v7 bv0[32])) +) +) |