You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
kahveciderin
changed the title
ConcolicFuzzer gives error
ConcolicFuzzer gives model is not available error
Feb 5, 2022
Describe the bug
Getting a model is not available error when using the ConcolicFuzzer
To Reproduce
Steps to reproduce the behavior:
Expected behavior
It should just work
Desktop (please complete the following information):
Additional context
Line 961 changing
output = subprocess.getoutput("z3 -t:60 " + f.name)
tooutput = subprocess.getoutput("z3 " + f.name)
, line 977 deletingassert o[1][0] == 'model'
and line 978 replacingreturn 'sat', {i[1]: (i[-1], i[-2]) for i in o[1][1:]}
withreturn 'sat', {i[1]: (i[-1], i[-2]) for i in o[1][0:]}
results in the ConcolicFuzzer working as expected.The text was updated successfully, but these errors were encountered: