Spurious lia failure: ZTautoChecker __ff __wit not true

[samuelgruetter]

We have a bedrock2 build that works for Coq 8.12, but fails for Coq master (95f7839) with the following error:

COQC /home/travis/build/mit-plv/bedrock2/compiler/src/compiler/ToplevelLoop.v
File "./theories/micromega/Lia.v", line 31, characters 23-36:
Error:
In environment
__p2, __p1 : Prop
__x3, __x2, __x1 : Z
__wit := [ZMicromega.CutProof
            (RingMicromega.PsatzAdd
               (RingMicromega.PsatzMulC (EnvRing.Pc (-1))
                  (RingMicromega.PsatzIn Z 2)) (RingMicromega.PsatzIn Z 0))
            (ZMicromega.RatProof
               (RingMicromega.PsatzAdd
                  (RingMicromega.PsatzMulE
                     (RingMicromega.PsatzC 18446744073709551616)
                     (RingMicromega.PsatzIn Z 0))
                  (RingMicromega.PsatzAdd
                     (RingMicromega.PsatzMulC (EnvRing.Pc (-1))
                        (RingMicromega.PsatzIn Z 3))
                     (RingMicromega.PsatzIn Z 1))) ZMicromega.DoneProof);
         ZMicromega.CutProof
           (RingMicromega.PsatzAdd (RingMicromega.PsatzIn Z 2)
              (RingMicromega.PsatzIn Z 0))
           (ZMicromega.RatProof
              (RingMicromega.PsatzAdd
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulE
                       (RingMicromega.PsatzC 18446744073709551616)
                       (RingMicromega.PsatzIn Z 0))
                    (RingMicromega.PsatzIn Z 2))
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn Z 4)
                    (RingMicromega.PsatzMulC (EnvRing.Pc (-1))
                       (RingMicromega.PsatzIn Z 3)))) ZMicromega.DoneProof)]
 : list ZMicromega.ZArithProof
__varmap := VarMap.Branch (VarMap.Elt __x2) __x1 (VarMap.Elt __x3)
 : VarMap.t Z
__ff := Tauto.IMPL
          (Tauto.IMPL
             (Tauto.A Tauto.isProp
                {|
                RingMicromega.Flhs := EnvRing.PEc 0;
                RingMicromega.Fop := RingMicromega.OpLt;
                RingMicromega.Frhs := EnvRing.PEc 18446744073709551616 |} tt)
             None
             (Tauto.AND
                (Tauto.A Tauto.isProp
                   {|
                   RingMicromega.Flhs := EnvRing.PEc 0;
                   RingMicromega.Fop := RingMicromega.OpLe;
                   RingMicromega.Frhs := EnvRing.PEX 1 |} tt)
                (Tauto.X Tauto.isProp __p1))) None
          (Tauto.IMPL
             (Tauto.IMPL
                (Tauto.NOT
                   (Tauto.A Tauto.isProp
                      {|
                      RingMicromega.Flhs := EnvRing.PEc 18446744073709551616;
                      RingMicromega.Fop := RingMicromega.OpEq;
                      RingMicromega.Frhs := EnvRing.PEc 0 |} tt)) None
                (Tauto.A Tauto.isProp
                   {|
                   RingMicromega.Flhs := EnvRing.PEadd 
                                           (EnvRing.PEX 2)
                                           (EnvRing.PEc 9223372036854775808);
                   RingMicromega.Fop := RingMicromega.OpEq;
                   RingMicromega.Frhs := EnvRing.PEadd
                                           (EnvRing.PEmul
                                              (EnvRing.PEc
                                                 18446744073709551616)
                                              (EnvRing.PEX 3))
                                           (EnvRing.PEX 1) |} tt)) None
             (Tauto.IMPL
                (Tauto.AND (Tauto.X Tauto.isProp __p2)
                   (Tauto.A Tauto.isProp
                      {|
                      RingMicromega.Flhs := EnvRing.PEX 2;
                      RingMicromega.Fop := RingMicromega.OpLt;
                      RingMicromega.Frhs := EnvRing.PEpow (EnvRing.PEc 2) 31 |}
                      tt)) None
                (Tauto.A Tauto.isProp
                   {|
                   RingMicromega.Flhs := EnvRing.PEsub 
                                           (EnvRing.PEX 1)
                                           (EnvRing.PEc 9223372036854775808);
                   RingMicromega.Fop := RingMicromega.OpEq;
                   RingMicromega.Frhs := EnvRing.PEX 2 |} tt)))
 : Tauto.BFormula (RingMicromega.Formula Z) Tauto.isProp
The term "eq_refl" has type "true = true" while it is expected to have type
 "ZMicromega.ZTautoChecker __ff __wit = true".

I tried to reproduce this problem locally by cloning Coq, checking out commit 95f7839, ./configure -local, make -j2, and then built bedrock2 using this Coq version, but the error was gone.
Could it be related to the OCaml version? Or to something else that differs between Travis CI and my laptop? Or are there any sources of non-determinism that could be relevant here?
/cc @fajb

[ejgallego]

What is the zarith version?

[samuelgruetter]

$ opam list zarith --installed
# Packages matching: installed & name-match(zarith)
# Name # Installed # Synopsis
zarith 1.10        Implements arithmetic and logical operations over arbitrary-precision integers

[ejgallego]

The version on Travis is 1.8.1 which is indeed buggy and won't work for Coq.

[ejgallego]

Duplicate of #13041

[fajb]

@ejgallego I am relieved...

[ejgallego]

@fajb yeah surprisingly old versions of zarith have quite strange bizarre behaviors.