Tiny simplification of constFoldProp

[blishko]

Description

I am trying to learn how different pieces of hevm work and concurrently learning Haskell.
Here is my attempt to simplify a piece of code using monadic operations.

• tested locally

[blishko]

I think we do not need to read the state again, because we have the information where any of the two disjunct is inconsistent in the results v1 and v2. We can use the old value of s.canBeSat, no?

[msooseth]

I think not, actually! The oneRun can change it! If you do git blame it kinda tries to show it... maybe not too well. But yeah, so it's actually not correct. Kind of a minefield. Maybe you could put a comment here, since I have also made this mistake and I have a feeling someone else may also bump into this.

[blishko]

Following up on our offline discussion.
After some exchange of ideas, I believe that updating the state here is unnecessary.
The reasoning is that the correct update already happens in go statements (if they are executed).
It goes like this:

• If both v1 and v2 are true, then both disjuncts are satisfiable, and neither go a or go b will be executed. So we just continue with the same state. No need for any update.

• Suppose that one of the variables is false, say v1, but the other is true.
  That means that disjunct a is unsatisfiable, b is satisfiable. The code will execute go b. That should just keep the variable canBeSat of the current state the same, because we already know this branch is satisfiable. And, the map with values will be updated (which is something that is actually not happening in main). So we do not have to touch the state, it is already OK.

• If both are unsatisfiable, both go b and go a will execute, and the latter will make the state unsat plus empty map. So again, no update is necessary afterwards.

[blishko]

@msooseth, I am gonna add more tests, and rename the method to isUnsat, because that is what the method actually checks, do you agree? It does not actually do constant folding.