Distinct domain constants with the same name.
MichaelRawson opened this issue · 1 comments
Refer to GEG001+1. The finite model produced contains
12.46/2.27 tff(finite_domain,axiom,
12.46/2.27 ! [X:$i] : (
12.46/2.27 X = jupiter | X = planet | X = named | X = named | X = continent
12.46/2.27 ) ).
12.46/2.27
12.46/2.27 tff(distinct_domain,axiom,
12.46/2.27 jupiter != planet & jupiter != named & jupiter != named & jupiter != continent & planet != named &
12.46/2.27 planet != named & planet != continent & named != named & named != continent & named != continent
12.46/2.27 ).
which suggests that there are two things called named
that are assumed distinct. @quickbeam123 says
So this is another issue for us to track and fix. I am guessing fmb starts internally working with two (formally) distinct "named"s, because, maybe, they end up in two different soft sorts. Then at printing time, the code does not bother to distinguish them (or use a fresh constant for at least one). This should be again easy to fix, once someone gets their hands dirty by delving into this part of the code.
Digging deeper, looks like this assertion would have failed in a debug configuration with named
. named
is assigned to constants 1 and 3.
Leaving this for someone with FMB expertise.