That picks up a further 428 occurrences Larry > On 14 Feb 2024, at 12:09, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de> wrote: > > "smt(z3" occurs seldom because z3 is the default for "smt", so often it's omitted. (I believe it used to be omitted and now it's explicit.) >