fuzzingbook
fuzzingbook copied to clipboard
ConcolicFuzzer gives `model is not available` error
Describe the bug Getting a model is not available error when using the ConcolicFuzzer
To Reproduce Steps to reproduce the behavior:
- Initialize the concolic fuzzer
- Write a simple program
- Fuzz that simple program with the concolic fuzzer
- You will get a model is not available error from z3
Expected behavior It should just work
Desktop (please complete the following information):
- OS: Archcraft (Arch Linux)
- Python version: 3.10.2
Additional context
Line 961 changing output = subprocess.getoutput("z3 -t:60 " + f.name)
to output = subprocess.getoutput("z3 " + f.name)
, line 977 deleting assert o[1][0] == 'model'
and line 978 replacing return 'sat', {i[1]: (i[-1], i[-2]) for i in o[1][1:]}
with return 'sat', {i[1]: (i[-1], i[-2]) for i in o[1][0:]}
results in the ConcolicFuzzer working as expected.