Getting NAN as trace even after using isnormal()

[Sunandan Adhikary]

HI,

I am trying to generate a trace for a program. As I was getting NaN as the value of the non_det float variable in trace I used isnormal() function to omit that trace. Still, it doesn't work! I am getting NaN in the trace. 

Is there any problem regarding nondet_float() function or there is any problem regarding isnormal() ?

Regards,

Sunandan Adhikary

[Michael Tautschnig]

Hello,

Would you be able to share an example program exhibiting the problem you described? Otherwise it is impossible to help you debug what is going wrong here.

Thanks,

Michael

--

---
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.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/CAMZfLepR95U%3Dcqv08eFuztv2_CXhEfJCPmU9u2g73t4Xsa0c3Q%40mail.gmail.com.

[Martin Nyx Brain]

On Tue, 2019-08-20 at 11:48 +0530, Sunandan Adhikary wrote:
> HI,

> I am trying to generate a trace for a program. As I was getting *NaN*
> as
> the value of the *non_det float variable* in trace I used* isnormal()
> *function
> to omit that trace. Still, it doesn't work! I am getting *NaN* in the
> trace.
> Is there any problem regarding *nondet_float()* function or there is
> any
> problem regarding *isnormal() *?

To echo what Michael said; without seeing the code it is very hard to
say. Even if the inputs are normal it is still very easy to generate
NaNs; that may be what is happening.

Cheers,
- Martin