fuzzingbook icon indicating copy to clipboard operation
fuzzingbook copied to clipboard

ConcolicFuzzer gives `model is not available` error

Open kahveciderin opened this issue 3 years ago • 0 comments

Describe the bug Getting a model is not available error when using the ConcolicFuzzer

To Reproduce Steps to reproduce the behavior:

  1. Initialize the concolic fuzzer
  2. Write a simple program
  3. Fuzz that simple program with the concolic fuzzer
  4. 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.

kahveciderin avatar Feb 05 '22 14:02 kahveciderin