Not able to emit loop invariant for a program.

[lahiri-phdworks]

Describe the bug

When using the --show-invars flags while invoking the program with sea pf, tool does not emit loop invariant. Please guide me here. Is this the correct output? I am using docker image build with llvm10-nightly.

To Reproduce
Steps to reproduce the behavior:

This is the input C file.

/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd();

int main(void) {
    int z1, z2, z3;

    int x = nd();
    int y = 0;

    while(y >= 0){
        y = y + x;
    }

    sassert(y >= 0);
}

Command I am running.

$ sea pf --horn-stats -g --show-invars --crab test.c

Logs, Stacktraces, and Screenshots

Output from from the tool.

usea@bea901793784:/examples/Documents/code_samples
$ sea pf --horn-stats -g --show-invars --crab example.c 
/usr/bin/clang-10 -c -emit-llvm -D__SEAHORN__ -fdeclspec -O1 -Xclang -disable-llvm-optzns -fgnu89-inline -m32 -I/home/usea/seahorn/include -g -o /tmp/sea-u2t3uqv2/example.bc example.c
/home/usea/seahorn/bin/seapp -o /tmp/sea-u2t3uqv2/example.pp.bc --simplifycfg-sink-common=false --strip-extern=false --promote-assumptions=false --kill-vaarg=true --horn-keep-arith-overflow=false /tmp/sea-u2t3uqv2/example.bc
/home/usea/seahorn/bin/seapp --simplifycfg-sink-common=false -o /tmp/sea-u2t3uqv2/example.pp.ms.bc --horn-mixed-sem --ms-reduce-main /tmp/sea-u2t3uqv2/example.pp.bc
/home/usea/seahorn/bin/seaopt -f --simplifycfg-sink-common=false -o /tmp/sea-u2t3uqv2/example.pp.ms.o.bc -O3 --seaopt-enable-indvar=false --seaopt-enable-loop-idiom=false --unroll-threshold=150 --unroll-allow-partial=false --unroll-partial-threshold=0 --vectorize-loops=false --disable-slp-vectorization=true /tmp/sea-u2t3uqv2/example.pp.ms.bc
/home/usea/seahorn/bin/seahorn --horn-crab --keep-shadows=true --sea-dsa=ci --horn-solve --horn-answer -horn-inter-proc -horn-sem-lvl=mem --horn-step=large /tmp/sea-u2t3uqv2/example.pp.ms.o.bc --horn-stats
CLAM WARNING: Call to external function verifier.nondet.sym.bound. Havocing the return value and possibly its modified memory regions if the pointer analysis models the external function
CLAM WARNING: Call to external function nd. Havocing the return value and possibly its modified memory regions if the pointer analysis models the external function
CLAM WARNING: Call to external function verifier.nondet.bool. Havocing the return value and possibly its modified memory regions if the pointer analysis models the external function
unsat
Function: main
main@entry: true
main@_3: true
main@verifier.error.split: false
main@empty.loop: true


************** BRUNCH STATS ***************** 
BRUNCH_STAT Result TRUE
BRUNCH_STAT Horn 0.00
BRUNCH_STAT HornClauseDB::loadZFixedPoint 0.00
BRUNCH_STAT HornifyModule 0.00
BRUNCH_STAT LargeHornifyFunction 0.00
BRUNCH_STAT seahorn_total 0.02
BRUNCH_STAT vcgen.store.clone 0.00
************** BRUNCH STATS END ***************** 

Desktop (please complete the following information):
Docker image build with llvm10-nightly

Additional context
Add any other context about the problem here.

[caballa]

The output is the expected one

Function: main
main@entry: true
main@_3: true
main@verifier.error.split: false
main@empty.loop: true

The option --show-invars shows the invariants inferred by Spacer. The invariants inferred by Crab (the abstract interpreter) are added as constraints (assumptions) to Spacer before Spacer starts. That's why they are not shown.
If you want to see the invariants inferred by crab you can use the option --log=crab. You should see something like this

Loading invariant main@entry()  true
Loading invariant main@.lr.ph(main@%.0.i3 main@%.01.i2 main@%loop.bound )  ((((((0-main@%loop.bound)<=0)&&((0+main@%loop.bound)<=0))&&((0-main@%.0.i3)<=0))&&((0-main@%.01.i2)<=-1))&&main@%_0)
Loading invariant main@verifier.error.split()  true
unsat
Function: main
main@entry: true
main@.lr.ph: true
main@verifier.error.split: false

Btw, please use branch dev14 which is our current development branch. There is a docker image for that.