Internal assertion failure when handling ternary expression #2000
Closed
Description
#include <assert.h>
#include <stdbool.h>
bool t2()
{
bool x;
return x;
}
bool t1()
{
return 1 == 2 && t2();
}
int main()
{
int nS;
int nE = t1();
bool x = nS ? nE ?: (nS > nE) : (nS < nE);
}CBMC
CBMC version 5.80.0 (cbmc-5.80.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000575161s
size of program expression: 41 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 4.0658e-05s
VERIFICATION SUCCESSFULESBMC
ESBMC version 7.6.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing test.c
Converting
Generating GOTO Program
esbmc: /root/workspace/ESBMC_Commit/esbmc_master/src/irep2/irep2_expr.h:1961: if2t::if2t(const type2tc&, const expr2tc&, const expr2tc&, const expr2tc&): Assertion `type->type_id == falseval->type->type_id' failed.
[1] 2891 IOT instruction ./esbmc test.c
Metadata
Assignees
Labels
No labels