gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

[TestComp-2022] Incompatibility Error #27

Closed DonggeLiu closed 2 years ago

DonggeLiu commented 2 years ago

Issue

Legion-SymCC terminated with status ERROR because of an incompatibility error in line 179.

Sample output from Legion-SymCC

Traceback (most recent call last):
  File "Legion.py", line 825, in <module>
    raise e
  File "Legion.py", line 743, in <module>
    prefix = node.sample()
  File "Legion.py", line 379, in sample
    sample = next(self.sampler)
  File "Legion.py", line 179, in naive
    KNOWN.add(value)
  File "/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c2a336d-6e52-4142-875a-30ab5a72506c/bin/legion-symcc-qUTt9O8WQk/dist/z3_solver-4.8.12.0-py3.9-linux-x86_64.egg/z3/z3.py", line 1013, in __eq__
  File "/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c2a336d-6e52-4142-875a-30ab5a72506c/bin/legion-symcc-qUTt9O8WQk/dist/z3_solver-4.8.12.0-py3.9-linux-x86_64.egg/z3/z3core.py", line 1723, in Z3_mk_eq
  File "/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c2a336d-6e52-4142-875a-30ab5a72506c/bin/legion-symcc-qUTt9O8WQk/dist/z3_solver-4.8.12.0-py3.9-linux-x86_64.egg/z3/z3core.py", line 1416, in Check
z3.z3types.Z3Exception: b'Sorts (_ BitVec 288) and (_ BitVec 384) are incompatible'

Command

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/product-lines/email_spec0_product36.cil.c

Sample program

product-lines/email_spec0_product36.cil.yml

gernst commented 2 years ago

should be fixed now