Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

Performance regression from 4.8.7 to 4.8.8 #4743

Closed
symphorien opened this issue Oct 19, 2020 · 2 comments
Closed

Performance regression from 4.8.7 to 4.8.8 #4743

symphorien opened this issue Oct 19, 2020 · 2 comments

Comments

@symphorien
Copy link

The following formula is solved in 0.715s (unsat) with 4.8.7 and times out in 4.8.8

(declare-fun __controlled_memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun y_8 () (_ BitVec 32))
(assert
(forall
 ((__control_index0 (_ BitVec 32)) (__control_memcell1 (_ BitVec 8))
  (__control_index2 (_ BitVec 32)) (__control_memcell3 (_ BitVec 32))
  (__control_index4 (_ BitVec 32)) (__control_memcell5 (_ BitVec 32))
  (__control_index6 (_ BitVec 32)) (__control_memcell7 (_ BitVec 32))
  (bs_unknown1_for_esp_32__4 (_ BitVec 32)) (ebp_21 (_ BitVec 32)))
 (let
 ((__memory_3_store_0
   (store __controlled_memory0 __control_index0 __control_memcell1)))
 (let
 ((__memory_3_store_1
   (store
   (store
   (store
   (store __memory_3_store_0 __control_index2
   ((_ extract 7 0) __control_memcell3)) (bvadd __control_index2 (_ bv1 32))
   ((_ extract 15 8) __control_memcell3)) (bvadd __control_index2 (_ bv2 32))
   ((_ extract 23 16) __control_memcell3))
   (bvadd __control_index2 (_ bv3 32))
   ((_ extract 31 24) __control_memcell3))))
 (let
 ((__memory_3_store_2
   (store
   (store
   (store
   (store __memory_3_store_1 __control_index4
   ((_ extract 7 0) __control_memcell5)) (bvadd __control_index4 (_ bv1 32))
   ((_ extract 15 8) __control_memcell5)) (bvadd __control_index4 (_ bv2 32))
   ((_ extract 23 16) __control_memcell5))
   (bvadd __control_index4 (_ bv3 32))
   ((_ extract 31 24) __control_memcell5))))
 (let
 ((__memory_3
   (store
   (store
   (store
   (store __memory_3_store_2 __control_index6
   ((_ extract 7 0) __control_memcell7)) (bvadd __control_index6 (_ bv1 32))
   ((_ extract 15 8) __control_memcell7)) (bvadd __control_index6 (_ bv2 32))
   ((_ extract 23 16) __control_memcell7))
   (bvadd __control_index6 (_ bv3 32))
   ((_ extract 31 24) __control_memcell7))))
 (let
 ((__memory_7
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store
   (store (store __memory_3 (_ bv134529040 32) (_ bv65 8)) (_ bv134529041 32)
   (_ bv65 8)) (_ bv134529042 32) (_ bv65 8)) (_ bv134529043 32) (_ bv65 8))
   (_ bv134529044 32) (_ bv65 8)) (_ bv134529045 32) (_ bv65 8))
   (_ bv134529046 32) (_ bv0 8)) (_ bv134529047 32) (_ bv0 8))
   (_ bv134529048 32) (_ bv0 8)) (_ bv134529049 32) (_ bv32 8))
   (_ bv134529050 32) (_ bv0 8)) (_ bv134529051 32) (_ bv0 8))
   (_ bv134529052 32) (_ bv0 8)) (_ bv134529053 32) (_ bv0 8))
   (_ bv134529054 32) (_ bv2 8)) (_ bv134529055 32) (_ bv0 8))
   (_ bv134529056 32) (_ bv255 8)) (_ bv134529057 32) (_ bv255 8))
   (_ bv134529058 32) (_ bv255 8)) (_ bv134529059 32) (_ bv255 8))
   (_ bv134529060 32) (_ bv71 8)) (_ bv134529061 32) (_ bv0 8))
   (_ bv134529062 32) (_ bv0 8)) (_ bv134529063 32) (_ bv0 8))
   (_ bv134529064 32) (_ bv0 8)) (_ bv134529065 32) (_ bv0 8))
   (_ bv134529066 32) (_ bv0 8)) (_ bv134529067 32) (_ bv0 8))
   (_ bv134529068 32) (_ bv0 8)) (_ bv134529069 32) (_ bv0 8))
   (_ bv134529070 32) (_ bv0 8)) (_ bv134529071 32) (_ bv0 8))
   (_ bv134529072 32) (_ bv0 8)) (_ bv134529073 32) (_ bv0 8))
   (_ bv134529074 32) (_ bv0 8)) (_ bv134529075 32) (_ bv0 8))
   (_ bv134529076 32) (_ bv0 8)) (_ bv134529077 32) (_ bv0 8))
   (_ bv134529078 32) (_ bv0 8)) (_ bv134529079 32) (_ bv0 8))
   (_ bv134529080 32) (_ bv0 8)) (_ bv134529081 32) (_ bv0 8))
   (_ bv134529082 32) (_ bv0 8)) (_ bv134529083 32) (_ bv0 8))
   (_ bv134529084 32) (_ bv0 8)) (_ bv134529085 32) (_ bv0 8))
   (_ bv134529086 32) (_ bv0 8)) (_ bv134529087 32) (_ bv0 8))))
 (let
 ((__memory_9
   (store
   (store
   (store
   (store __memory_7 (bvadd __control_index4 (_ bv4 32))
   ((_ extract 7 0) y_8)) (bvadd __control_index4 (_ bv5 32))
   ((_ extract 15 8) y_8)) (bvadd __control_index4 (_ bv6 32))
   ((_ extract 23 16) y_8)) (bvadd __control_index4 (_ bv7 32))
   ((_ extract 31 24) y_8))))
 (let
 ((res32_11 (bvand (bvsub __control_index4 (_ bv4 32)) (_ bv4294967280 32))))
 (let
 ((__memory_19
   (let
   ((elt_da423a8
     (concat (select __memory_3 (bvsub __control_index4 (_ bv1 32)))
     (concat (select __memory_3 (bvsub __control_index4 (_ bv2 32)))
     (concat (select __memory_3 (bvsub __control_index4 (_ bv3 32)))
     (select __memory_3 (bvsub __control_index4 (_ bv4 32))))))))
   (store
   (store
   (store
   (store __memory_9 (bvsub res32_11 (_ bv4 32))
   ((_ extract 7 0) elt_da423a8)) (bvsub res32_11 (_ bv3 32))
   ((_ extract 15 8) elt_da423a8)) (bvsub res32_11 (_ bv2 32))
   ((_ extract 23 16) elt_da423a8)) (bvsub res32_11 (_ bv1 32))
   ((_ extract 31 24) elt_da423a8)))))
 (let
 ((__memory_22
   (store
   (store
   (store
   (store __memory_19 (bvsub res32_11 (_ bv8 32)) ((_ extract 7 0) ebp_21))
   (bvsub res32_11 (_ bv7 32)) ((_ extract 15 8) ebp_21))
   (bvsub res32_11 (_ bv6 32)) ((_ extract 23 16) ebp_21))
   (bvsub res32_11 (_ bv5 32)) ((_ extract 31 24) ebp_21))))
 (let
 ((__memory_25
   (let ((elt_855d08d (bvadd bs_unknown1_for_esp_32__4 (_ bv4 32))))
   (store
   (store
   (store
   (store __memory_22 (bvsub res32_11 (_ bv12 32))
   ((_ extract 7 0) elt_855d08d)) (bvsub res32_11 (_ bv11 32))
   ((_ extract 15 8) elt_855d08d)) (bvsub res32_11 (_ bv10 32))
   ((_ extract 23 16) elt_855d08d)) (bvsub res32_11 (_ bv9 32))
   ((_ extract 31 24) elt_855d08d)))))
 (let
 ((res32_37
   (bvand
   (concat (select __memory_25 (bvadd bs_unknown1_for_esp_32__4 (_ bv7 32)))
   (concat (select __memory_25 (bvadd bs_unknown1_for_esp_32__4 (_ bv6 32)))
   (concat (select __memory_25 (bvadd bs_unknown1_for_esp_32__4 (_ bv5 32)))
   (select __memory_25 (bvadd bs_unknown1_for_esp_32__4 (_ bv4 32))))))
   (_ bv3 32))))
 (=>
 (and (= (bvsub __control_index0 (_ bv134529040 32)) res32_37)
 (and (= (bvsub __control_index2 (_ bv4 32)) __control_index4)
 (and (bvuge (bvsub __control_index4 (_ bv4 32)) (_ bv4293918720 32))
 (and (= (bvsub __control_index4 (_ bv4 32)) bs_unknown1_for_esp_32__4)
 (= __control_index6 bs_unknown1_for_esp_32__4)))))
 (and (= (select __memory_7 (bvadd res32_37 (_ bv134529040 32))) (_ bv65 8))
 (=
 (concat (select __memory_25 (bvadd __control_index4 (_ bv7 32)))
 (concat (select __memory_25 (bvadd __control_index4 (_ bv6 32)))
 (concat (select __memory_25 (bvadd __control_index4 (_ bv5 32)))
 (select __memory_25 (bvadd __control_index4 (_ bv4 32)))))) res32_37))))))))))))))))
(check-sat)
NikolajBjorner added a commit that referenced this issue Oct 30, 2020
@NikolajBjorner
add parameter for scenario from #4743
f354671
@NikolajBjorner
Copy link
Contributor

This specifically requires blasting select/stores into if-then-else.
Generally, it is too expensive to expand up front. I am adding a configuration that you can use to force blasting.

Default behavior:

z3 4743.smt2 -v:2 rewriter.blast_select_store=false -T:3

Behavior that works for you

z3 4743.smt2 -v:2 rewriter.blast_select_store=true

@symphorien
Copy link
Author

Thanks.
I was mainly surprised by such a difference in a point release, but I guess it can't be helped.

nescio007 added a commit to nescio007/teether that referenced this issue Jul 27, 2021
@nescio007
Fix issues with new z3 versions
35dcf93 
starting from z3 version 4.8.8, some tests of teEther began to fail.
It appears that a change z3's array handling was responsible for this behaviour, which caused z3 to output `unknown` instead of `sat`/`unsat` for some cases.
A similar issue was reported as Z3Prover/z3#4743, and z3 v4.8.10 introduced a new parameter `rewriter.blast_select_store`, which re-enables the old default behaviour (Z3Prover/z3@f354671).
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @symphorien