Feature Request: Replacing uninterpreted functions for a branch

[jfh1911]

I am using korn to only generate the CHCs for a svcomp-task.

Currently, Korn generates a new uninterpreted function (e.g. $main_if1) for a branch. As far as i understood it, these predicates are summarizing the branch (similar to loop invariant).

As (at least in my use-case) each new predicate increases the complexity, it would be great to have an option to not generate these predicates but create two separate formulae (one if-branch and one -else branch), both continuing with the next statement

For this small example ex.c (as txt due to upload rules), which is

int main() {
  int i = 0;
  int j = 0;
  int l = 1;
  if(l==2){
    i = i + 1;
  }
  else {
    j = j+1;
  }

  assert((i+j) == l);
  return 0;
}

(which contains dead code in the if branch, i know)

It would be great if korn is able to generate two fomulae:

; if then  --> assert (= (+ i1 j2) l3)
(assert
     (=> (and (= l3 1)
             (= j2 0)
             (= i1 0)
             (= l3 2))
      (not (= (+ (+ i1 1) j2) l3))
        false))

; if else --> assert (= (+ i1 j2) l3)
((assert
     (=> (and (= l3 1)
             (= j2 0)
             (= i1 0)
             (not (= l3 2)))
      (not (= (+ i1 (+ j2 1)) l3))
        false))

This makes the verification process (at least in my usecase) easier.

[gernst]

Yes, this is definitely planned, and there is some preliminary work on branch exec, but afaik it's currently not working right. Feel free to try it!

[jfh1911]

FYI: I tried it with the example below, got:

program:      /home/jan/Documents/ig-framework/tooling/framework/igml/output/logs/svcomp21-loops__for_bounded_loop1/simplified.c
clauses:      /home/jan/Documents/ig-framework/tooling/framework/igml/output/logs/svcomp21-loops__for_bounded_loop1/simplified.smt2
error:        not implemented korn.horn.Proc.local (Proc.scala:153)

Example as txt file: simplified.c.txt (Simplified version from SV-COMP loops/for_bounded_loop.yml )