Skip to content

Releases: westtide/korn

v1.0

08 Jun 09:09
@westtide westtide
c2chc
f59c05c
This commit was signed with the committer’s verified signature.
westtide westtide
GPG key ID: DD3E1F9565DFFDA0
Verified
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.0 Latest
Latest

Release Notes

New Features

  • Added support for the -c2chc flag in the Korn.jar application. This new feature allows users to translate C code into Constrained Horn Clauses (CHC) formula.

How to Use

  • To use this feature, run the Korn.jar application with the -c2chc flag followed by the path to the C file you want to translate. For example: java -jar Korn.jar --c2chc 1.c

This command will translate the C code in 1.c into a CHC formula and write the result to an SMT2 file named 1.smt2.

Compatibility

  • The generated SMT2 file is compatible with the Eldarica solver and Z3: (set-logic HORN)

Notes

  • Please ensure that the Eldarica solver or Z3 is installed and properly configured on your system to use the generated SMT2 file.
  • z3 1.smt2
  • java -jar Eldarica.jar 1.smt2
Assets 3
Loading