Z3 not working with floating values

[Ipsita Koley]

With z3 installed in my system, I tried to verify the following code snippet using CBMC with --z3 option

float nondet_float();

int main()

{

float a,b,c;

a = nondet_float();

b = nondet_float();

c= a + b;

assert(c<=0 && c>=1);

}

It is giving the following error:

Starting Bounded Model Checking

size of program expression: 37 steps

simple slicing removed 5 assignments

Generated 1 VCC(s), 1 remaining after simplification

Passing problem to SMT2 QF_AUFBV using Z3

converting SSA

Segmentation fault (core dumped)

Can anyone please help?

[Martin Nyx Brain]

Which version of the tool are you using? Have you tried the develop
branch of https://github.com/diffblue/cbmc/ ?

Cheers,
- Martin

[Ipsita Koley]

Was using the binaries.

Downloaded the source from GitHub, but its giving the following error:

## Entering big-int

make  -C big-int

make[1]: Entering directory '/home/user/Documents/Softwares/cbmc-develop/src/big-int'

make[1]: Nothing to be done for 'first_target'.

make[1]: Leaving directory '/home/user/Documents/Softwares/cbmc-develop/src/big-int'

## Entering util

make  -C util

make[1]: Entering directory '/home/user/Documents/Softwares/cbmc-develop/src/util'

fatal: Not a git repository (or any parent up to mount point /home/user)

Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).

make[1]: Nothing to be done for 'first_target'.

make[1]: Leaving directory '/home/user/Documents/Softwares/cbmc-develop/src/util'

## Entering langapi

make  -C langapi

make[1]: Entering directory '/home/user/Documents/Softwares/cbmc-develop/src/langapi'

make[1]: Nothing to be done for 'first_target'.

make[1]: Leaving directory '/home/user/Documents/Softwares/cbmc-develop/src/langapi'

## Entering ansi-c

make  -C ansi-c

make[1]: Entering directory '/home/user/Documents/Softwares/cbmc-develop/src/ansi-c'

flex -Pyyansi_c -oansi_c_lex.yy.cpp scanner.l

make[1]: flex: Command not found

Makefile:88: recipe for target 'ansi_c_lex.yy.cpp' failed

make[1]: *** [ansi_c_lex.yy.cpp] Error 127

make[1]: Leaving directory '/home/user/Documents/Softwares/cbmc-develop/src/ansi-c'

Makefile:75: recipe for target 'ansi-c.dir' failed

make: *** [ansi-c.dir] Error 2

Regards,

Ipsita

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Martin Nyx Brain]

Looks like you haven't got flex installed; have a look at COMPILING.md
for the prerequites.

Cheers,
- Martin