Right on. Consider whether forcing someone to unlock their smartphone should constitute compelled self-incrimination. This is a problem that US courts have flip-flopped on. [0] How would an SMT solver derive answer? It can't. You'd need a general AI.

Even ignoring the subtleties of the real world that the ̶l̶a̶w̶ edit legal system must cope with, nuts-and-bolts legal concepts like mens rea can't be mapped to algebraic expressions.

[0] https://arstechnica.com/tech-policy/2020/06/indiana-supreme-...

Yes but you can do a what-if analysis based on the parameter $degree being equal to 'gross', 'egregious' or 'blatant'.