Seahorn gives SAT, but the harness failed to show assertion violation.

[pkalita595]

Describe the bug

For the following loop-free program, I am getting SAT from Seahorn, but when I execute the binary with the generated counter-example, it doesn't emit __VERIFIER_error was executed. You can see that when I print the ssassert condition, I get 1 (see last print statement), which shows that the assertion (sassert) is not violated by the generated counter-example. I am curious why I am getting SAT in this case and why the counter-example is not able to show assertion violation. I have also tried with the --bmc flag and it also shows the same behavior. It will be helpful if I get to know how to debug this kind of error.

#include "seahorn/seahorn.h"
#include<stdio.h>

extern float nd(void);

float Abs(float x){
    return x >= 0 ? x : -x;
}

int main(void){
        float in_0 = nd();
        float in_1 = nd();
        float out_0;
        float out_1;
        float out_2;

        float in  = nd();
        float out = in >=0 ? in: 0;
        float l_out, u_out, xx;

        float l_in = in_0 - Abs(in_1);
        float u_in = in_0 + Abs(in_1);

        assume(u_in - l_in > 0.0);

        assume(l_in <= in && in <= u_in);

        if(u_in <= 0){
                printf("If statement taken\n");
                out_0 = 0; out_1 = 0; out_2 = 0;
        }

        l_out = out_0 - Abs(out_1) - Abs(out_2);
        u_out = out_0 + Abs(out_1) + Abs(out_2);

        printf("l_out: %f, u_out: %f, out: %f, ssasert: %d\n", l_out, u_out, out, l_out <= out && out <= u_out);
        sassert(l_out <= out && out <= u_out);
}

To Reproduce
Steps to reproduce the behavior:

1. Link to an input file (bitcode is preferred): See above
2. Full command line options: List of commands I have executed.

sea pf test.c --cex=test.ll --show-invars -m64
sea exe -m64 -g test.c test.ll -o out
./out

Output:

/usr/bin/clang-10 -c -emit-llvm -D__SEAHORN__ -fdeclspec -O1 -Xclang -disable-llvm-optzns -fgnu89-inline -m32 -I/home/usea/seahorn/include -o /tmp/sea-2ll8m3da/test.bc test.c
/home/usea/seahorn/bin/seapp -o /tmp/sea-2ll8m3da/test.pp.bc --simplifycfg-sink-common=false --strip-extern=false --promote-assumptions=false --kill-vaarg=true --horn-keep-arith-overflow=false /tmp/sea-2ll8m3da/test.bc
/home/usea/seahorn/bin/seapp --simplifycfg-sink-common=false -o /tmp/sea-2ll8m3da/test.pp.ms.bc --horn-mixed-sem --ms-reduce-main /tmp/sea-2ll8m3da/test.pp.bc
/home/usea/seahorn/bin/seaopt -f --simplifycfg-sink-common=false -o /tmp/sea-2ll8m3da/test.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-2ll8m3da/test.pp.ms.bc
/home/usea/seahorn/bin/seahorn --keep-shadows=true --sea-dsa=ci --horn-solve --horn-answer -horn-cex-pass -horn-cex=test.ll -horn-inter-proc -horn-sem-lvl=mem --horn-step=large /tmp/sea-2ll8m3da/test.pp.ms.o.bc
sat
main@verifier.error.split
main@verifier.error.split --> query!0
/usr/bin/clang-10 -c -emit-llvm -D__SEAHORN__ -fdeclspec -O1 -Xclang -disable-llvm-optzns -fgnu89-inline -m64 -I/home/usea/seahorn/include -g -o /tmp/tmp-69ghniw6/test.bc test.c
/usr/bin/llvm-link-10 -o /tmp/sea-_81kb80y/merged.bc /tmp/tmp-69ghniw6/test.bc test.ll
warning: Linking two modules of different data layouts: 'test.ll' is 'e-m:e-p:32:32-p270:32:32-p271:32:32-p272:64:64-f64:32:64-f80:32-n8:16:32-S128' whereas 'llvm-link' is 'e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128'

/home/usea/seahorn/bin/seapp -o /tmp/sea-_81kb80y/merged.ext.bc --simplifycfg-sink-common=false --only-strip-extern=true --keep-lib-fn /tmp/sea-_81kb80y/merged.bc
/home/usea/seahorn/bin/seapp -o /tmp/sea-_81kb80y/merged.ext.int.bc --simplifycfg-sink-common=false --klee-internalize /tmp/sea-_81kb80y/merged.ext.bc
/home/usea/seahorn/bin/seapp -o /tmp/sea-_81kb80y/merged.ext.int.wmem.bc --wrap-mem /tmp/sea-_81kb80y/merged.ext.int.bc
/usr/bin/clang++-10 -m64 -g -o out /tmp/sea-_81kb80y/merged.ext.int.wmem.rmtf.bc /home/usea/seahorn/lib/libsea-rt.a
If statement taken
l_out: 0.000000, u_out: 0.000000, out: 0.000000, ssasert: 1

Seahorn version
I am using the seahorn docker created by the authors (https://github.com/seahorn/seahorn#installation). Showing below the seahorn version.

$ seahorn --version
LLVM (http://llvm.org/):
  LLVM version 10.0.1
  
  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: skylake

SeaHorn (http://seahorn.github.io/):
  SeaHorn version 10.0.0-rc0-3bf79a59

[agurfinkel]

SeaHorn does not support float/double type. They are abstracted as non-deterministic.