diff --git a/test/python/test_proof_trace.py b/test/python/test_proof_trace.py index 4e857b4e8..dfe2997b4 100644 --- a/test/python/test_proof_trace.py +++ b/test/python/test_proof_trace.py @@ -3,6 +3,7 @@ # RUN: export IN=$(realpath Inputs/proof-trace.in) # RUN: cd %t && %kompile "$KORE_DEF" main --proof-hint-instrumentation -o interpreter # RUN: rm -f proof_trace.bin && ./interpreter "$IN" -1 proof_trace.bin --proof-output +# RUN: kore-rich-header "$KORE_DEF" > %t/header.bin # RUN: %python %s @@ -19,9 +20,13 @@ def test_file(self): binary_proof_trace = os.path.join( os.path.dirname(os.path.realpath(__file__)), "Output", "test_proof_trace.py.tmp", "proof_trace.bin") + binary_header_path = os.path.join( + os.path.dirname(os.path.realpath(__file__)), + "Output", "test_proof_trace.py.tmp", "header.bin") + header = kllvm.prooftrace.kore_header(binary_header_path) with open(binary_proof_trace, 'rb') as f: data = f.read() - trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data) + trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data, header) self.assertFalse(trace is None) # check that there is a initial configuration diff --git a/test/python/test_proof_trace_slow.py b/test/python/test_proof_trace_slow.py index 947520f72..ce0368682 100644 --- a/test/python/test_proof_trace_slow.py +++ b/test/python/test_proof_trace_slow.py @@ -3,6 +3,7 @@ # RUN: export IN=$(realpath Inputs/proof-trace.in) # RUN: cd %t && %kompile "$KORE_DEF" main --proof-hint-instrumentation-slow -o interpreter # RUN: rm -f proof_trace.bin && ./interpreter "$IN" -1 proof_trace.bin --proof-output +# RUN: kore-rich-header "$KORE_DEF" > %t/header.bin # RUN: %python %s @@ -19,9 +20,13 @@ def test_file(self): binary_proof_trace = os.path.join( os.path.dirname(os.path.realpath(__file__)), "Output", "test_proof_trace_slow.py.tmp", "proof_trace.bin") + binary_header_path = os.path.join( + os.path.dirname(os.path.realpath(__file__)), + "Output", "test_proof_trace_slow.py.tmp", "header.bin") + header = kllvm.prooftrace.kore_header(binary_header_path) with open(binary_proof_trace, 'rb') as f: data = f.read() - trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data) + trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data, header) self.assertFalse(trace is None) # check that there is a initial configuration