vprover/vampire

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.