diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 16:12:06 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 16:12:06 +0000 |
| commit | b3d6d0ccc76e92304fe612b23dc76a7d78061567 (patch) | |
| tree | a609abc331ec31f3188dfa15a22d68835edd5b1c /test/regress/regress0/aufbv | |
| parent | fbaa1e2bdb2d10465b76fc6fc3fbfd3318612493 (diff) | |
cleaning up the expample for the future
Diffstat (limited to 'test/regress/regress0/aufbv')
| -rw-r--r-- | test/regress/regress0/aufbv/diseqprop.01.smt | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/test/regress/regress0/aufbv/diseqprop.01.smt b/test/regress/regress0/aufbv/diseqprop.01.smt index 543684e21..4b3130475 100644 --- a/test/regress/regress0/aufbv/diseqprop.01.smt +++ b/test/regress/regress0/aufbv/diseqprop.01.smt @@ -1,12 +1,13 @@ (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])) -) + + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :extrafuns ((a Array[32:8])) + + :assumption (not (= (store a x bv0[8]) (store a x (extract[7:0] y)))) + :assumption (= y bv0[32]) + + :formula true ) |