wrong output for programs with printf function

[akhutail]

Input C file contents-
#include <stdio.h> int main(){ printf("hello"); return 0; }
and
#include <stdio.h> int main(){ printf("bye"); return 0; }

./llreve -I /usr/lib/gcc/x86_64-linux-gnu/7/include/ " + "./"+file+ " ./teacher_solution.c -o reve.smt2
Output-
(set-logic HORN) (define-fun .str$1 () Int (- 5)) (define-fun .str$2 () Int (- 5)) (define-fun INV_REC_printf^printf ((_$1_0 Int) (_$2_0 Int) (result$1 Int) (result$2 Int)) Bool (=> (= _$1_0 _$2_0) (= result$1 result$2))) (define-fun INV_REC_printf__1 ((_$1_0 Int) (result$1 Int)) Bool true) (define-fun INV_REC_printf__2 ((_$2_0 Int) (result$2 Int)) Bool true) (define-fun IN_INV () Bool true) (define-fun OUT_INV ((result$1 Int) (result$2 Int)) Bool (= result$1 result$2)) (assert (forall ((call$1_0 Int) (call$2_0 Int)) (=> (INV_REC_printf^printf (+ .str$1 (* 4 0) 0) (+ .str$2 (* 6 0) 0) call$1_0 call$2_0) (let ((result$1 0) (result$2 0)) (OUT_INV result$1 result$2))))) (check-sat) (get-model)

./z3 fixedpoint.engine=duality -T:300 reve.smt2
Output-
sat (model (define-fun @Fail!0 () Bool false) )

[StephanGocht]

By default, functions are assumed to have no side effect. You are not using the return value of printf. Hence, the programs are equal because the side effect of printing text is not observable given our abstraction. There are two work arrounds for this: (a) make use of the return value of printf and let it influence the return value of the program. (b) use the parameter -heap. In this case printf may change the heap and llreve will require that the heaps of both programs are the same, which it can only ensure if both programs call printf with the same value.

But there is another issue: Strings are abstracted away. I am not sure what the intended meaning is, might be heap locations, but it does not change with string length... It might be something like first string of the program, second string of the program, etc. This means that in your example there is no difference between "hello" and "bye" because they are both the first string of the program. I would consider this a bug, that should be fixed. Again, we can work around this by defining all string constants from both programs in advance.

The program

const char * a = "a";
const char * b = "b";

#include <stdio.h>

int main(){printf("a"); return 0;}

and

const char * a = "a";
const char * b = "b";

#include <stdio.h>

int main(){printf("b"); return 0;}

should work as intended when calling llreve with -heap.

My current impression is that string support is not very stable. Maybe @cocreature can say more about this.

[akhutail]

Thanks for reply. These workarounds should be sufficient for my need.