crash and wrong smtlib logic

[florianschanda]

Hi,

I am trying to refresh some benchmarks.

On the following file (from the rosa benchmark suite) there are several problems.

#include <math.h>

double triangle1(double a, double c, double b) {
  __CPROVER_assume(1.0 <= a && a <= 9.0);
  __CPROVER_assume(1.0 <= b && b <= 9.0);
  __CPROVER_assume(1.0 <= c && c <= 9.0);
  __CPROVER_assume(a + b > c + 0.1);
  __CPROVER_assume(a + c > b + 0.1);
  __CPROVER_assume(b + c > a + 0.1);
  double s = (((a + b) + c) / 2.0);
  double res = sqrt((((s * (s - a)) * (s - b)) * (s - c)));
  __CPROVER_assert(0.29 <= res && res <= 35.1, "postcondition");
  return res;
}

(1) There is a crash

$ cbmc --smt2 --fpa triangle1.c --function triangle1
CBMC version 6.9.0 (cbmc-6.9.0) 64-bit x86_64 linux
Type-checking triangle1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV (with FPA) using Z3
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:4962 function: flatten2bv
Condition: !use_FPA_theory
Reason: floatbv expressions should be flattened when using FPA theory
Backtrace:
...

(2) The wrong logic is set (QF_AUFBV does not include FP, it should be QF_AUFBVFP).

(3) Ideally the smtlib version emitted could be 2.6, not 2.5 since CVC5 does not support 2.5 at all anymore. Since you're not using DT, this should be as simple as just changing the version number in the output.