Non-deterministic compare

[BrunoDutertre]

In run_code, the evaluation of compare uses pointer comparison.

This looks like undefined C/C++ behavior.

It also means that the semantics of compare is not well defined and
that running the same code is not deterministic. Results may depend
on how symbols are stored in memory.

Example:

(declare sort type)
(declare x sort)
(declare y sort)
(run (compare x y 1 0))

On my computer, the result is 0 in most cases, but once in a while, it's 1:

[Running-sc (compare x y 1 0)] = 
0
Proof checked successfully!

time = 115
sym count = 0
marked count = 0

[Running-sc (compare x y 1 0)] = 
1
Proof checked successfully!

time = 189
sym count = 0
marked count = 0

[ajreynol]

I agree this is not ideal behavior.

In detail, the side condition primitive compare was introduced for this paper: https://homepage.divms.uiowa.edu/~ajreynol/report-lra-pf.pdf as a way of introducing an arbitrary ordering on variables. This is used for e.g. polynomial normalization. The use of pointer comparison was done intentionally, but indeed it makes LFSC non-deterministic.

I am considering eliminating this primitive from the language altogether, since it is not necessary in the new signature.

[BrunoDutertre]

If I have a vote on this: remove. Simpler is better.

Bruno