Apron analysis does not support trivial assertions

[sim642]

The output of

./regtest.sh 78 02 --trace apron

contains

%%% apron: assert_constraint 1 > 0 unsupported: Exp_not_supported
%%% apron: assert_constraint 1 < 0 unsupported: Exp_not_supported
[...]
%%% apron: assert_constraint 1 != 0 unsupported: Exp_not_supported

This is odd because there's nothing complicated or problematic (e.g. overflows) with them. Asserting the first one is of course useless (it refines nothing), which is also what currently happens with unsupported expressions (but it would be nice to not have spurious messages like this). Asserting the second one should refine to bottom, instead of remaining unchanged (we're missing the most precise possible result!).

[michael-schwarz]

My guess is that our expression translation does simply not translate constants to assertions. I also don't know what we expect to find here, given that we almost never run Goblint without at least constant propagation enabled, and the refinement to bottom happens at the analysis product level.

[sim642]

The program doesn't contain expressions like 1 > 0 though. These are something the relational analysis itself conjures up somewhere.

[michael-schwarz]

I guess it's what happens with Pos(1) internally.