diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-10 03:03:17 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-10 03:03:17 +0000 |
| commit | e761ec344a7c9d9b5bff5f312cdb8932083e0bc8 (patch) | |
| tree | 8a936c4e0c22cf45ec33d6f87a7bc01f31ab49cd /test/regress/regress0/aufbv | |
| parent | 3d1c71026c7b8aaa2e9689d27415d80c412ece2e (diff) | |
fixes for bug347
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
Diffstat (limited to 'test/regress/regress0/aufbv')
| -rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/aufbv/bug347.smt | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index bdcaaa2d0..bec83183a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -13,6 +13,7 @@ MAKEFLAGS = -k TESTS = \ bug00.smt \ bug338.smt2 \ + bug347.smt \ try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ diseqprop.01.smt \ wchains010ue.delta01.smt \ diff --git a/test/regress/regress0/aufbv/bug347.smt b/test/regress/regress0/aufbv/bug347.smt new file mode 100644 index 000000000..f467cd4b3 --- /dev/null +++ b/test/regress/regress0/aufbv/bug347.smt @@ -0,0 +1,11 @@ +(benchmark B_ + :status sat + :category { unknown } + :logic QF_AUFBV + :extrafuns ((delete_0_val_1 BitVec[32])) + :extrafuns ((delete_0_curr_6 BitVec[32])) + :extrafuns ((arr_next_13 Array[32:32])) + :extrafuns ((arr_next_14 Array[32:32])) + :extrafuns ((delete_0_head_1 BitVec[32])) + :formula (and (= bv0[32] (ite (= bv0[32] delete_0_head_1) (select arr_next_14 delete_0_curr_6) delete_0_curr_6)) (= arr_next_14 arr_next_13) (= bv1[32] (select arr_next_13 bv1[32])) (= delete_0_curr_6 (ite (= bv0[32] delete_0_val_1) bv0[32] bv1[32]))) +) |