Including time spent on get_model() into solving time

[ChengyuSong]

trafficstars

My own experience: check() is much faster than get_model(). Maybe we need to change the tactics to solve this issue.

[insuyun]

Nope. Do you have a benchmark or an example for this issue?

[ChengyuSong]

On LAVA-M, uniq, using fuzzer_input/TODO, when I tried to flip all symbolic branches. If I only do check(), it takes my tool 31s. But if I enable get_model(), it won't finish after 5~6 min.

Maybe you can compare the result of including and excluding the time spent on get_model and see.

[insuyun]

Sorry, but how can I get concrete inputs without calling get_model()?

[ChengyuSong]

You cannot, I found this because I thought it should be very fast, but it wasn't. So I tried to figure out where's bottleneck, taint, expression construction, check, get_model, or I/O. It turns out to be get_model(). And I don't have a good solution other than filtering branches :(

[insuyun]

As you already know, QSYM also filters some branches similar to AFL. Also, I don't have any idea how to solve this. But it is very interesting observation. Let's keep this issue and resolve it if we have a good solution for this. Thank you, Chengyu.

[ChengyuSong]

Sounds good. I'll read more about Z3 configurations and ask around.