Preserve sat counterexamples on universal-quantification VCs

[julesmt]

LoopElim, CallElim, and frontEndPhase demote every sat counterexample
via a fun _ => false validator stub. For universal-quantification
obligations (loop-invariant maintenance/entry, measure bounds, callee
postcondition), any witness in the abstracted domain is already in the
user's stated domain, so the demotion is unnecessary.

Adds obligationLabelIsUniversal and wires it as the first branch of
each phase's getValidation. Universal labels preserve the model;
everything else still demotes.

Closes part of #1324.

[atomb]

It looks like a couple of tests are failing, but in a way that I think just confirms that your fix had the intended behavior. They'll just need to have their expected output updated.

[atomb]

Can you update the target branch to main2? We're not merging changes to main for the next week or so unless they're related to splitting the repo into multiple pieces.

[julesmt]

Sorry I rushed and forgot to commit the expected files for the tests. I will update all that

[aqjune-aws]

I have one structural comment and one more interesting comment.
For the former one - I think it should be the individual PipelinePhase objects that recognize the structure of the new assertion names, because this will correspond to the implementation detail of each pass. For example, the label names generated by LoopElim must be listed near the PipelinePhase object for LoopElim, not globally.

The more interesting question is, let's assume that we have a program like this, with a loop whose invariant is somewhat incompletely annotated:

  int x = 0, y = 1      
  while (x < 10) { // loop invariant: x > 0
    y += 1
    x += y       
  }                                                                                                                                                                                                                                                                                                                                                                     

Since the loop invariant didn't mention y > 0, the check I /\ G ==> I can raise a spurious error message saying that 'oh, x > 0 won't hold when x = 0 and y = -1!'. However, this isn't in the possible behavior set of this program.
On the other hand, if we interpret simply the assertion as what we want to check, this is a true counterexample of I /\ G ==> I.

However, I am leaning towards Strata always providing concrete counterexamples that can be reproduced in the original source program (hence the first interpretation among the two options). Then this will make the goal of reducing ? hard, which will make you sad. :( Are there any possible workarounds that you can think about?