Better spreading SMT solver load?

[chadbrewbaker]

I was playing with zstd yesterday. The Makefile is easy to play with, just do:

# sudo service redis-server start  # Remember to turn Redis on.
 CC=$SOUPER_BIN/sclang make -j

(Aside) The zstd runtime was worse worse with Souper. Is Souper is breaking cache boundaries or branch predictions?

I noticed Souper had a really hard time spreading load across cores when compiling a wllvm fat IR file.

# What I remember running, might have a typo
LLVM_COMPILER=clang CC=wllvm make -j
extract-bc pkg-config
$SOUPER_BIN/sclang pkg-config.bc

Is there a flag I am missing to break Z3 solves into smaller chunks, or should I noodle on a PR?

Also, similer to gcc -fverbose-asm, how would you get the optimizations Souper produces printed as assembler comments?