Literal True condition causes assertion

[senier]

The following specification

package Test is
   type T is mod 2 ** 8;
   type Msg is
      message
         F1 : T
            then F2
               if True;
         F2 : T;
      end message;
end Test;

results in a bug box

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.5.1.dev484+g0daf4858
RecordFlux-parser 0.11.0
attrs 21.4.0
ruamel.yaml 0.17.21
pydotplus 2.0.2
icontract 2.6.2
z3-solver 4.11.1.0
pydantic 1.9.2

Optimized: True

Command: /home/senier/Devel/RecordFlux_issue_review-2022-08-24/.venv/bin/rflx check test.rflx

Traceback (most recent call last):
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/cli.py", line 209, in main
    args.func(args)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/cli.py", line 250, in check
    parse(args.files, args.no_verification, args.workers)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/cli.py", line 311, in parse
    model = parser.create_model()
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/specification/parser.py", line 1643, in create_model
    self._evaluate_specification(error, spec_node.spec, spec_node.filename)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/specification/parser.py", line 1701, in _evaluate_specification
    new_type = handlers[t.f_definition.kind_name](
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/specification/parser.py", line 867, in create_message
    result = create_proven_message(
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/specification/parser.py", line 1377, in create_proven_message
    proven_message = unproven_message.proven(
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/model/message.py", line 2062, in proven
    return Message(
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/model/message.py", line 837, in __init__
    self.verify()
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/model/message.py", line 843, in verify
    self._verify_expression_types()
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/model/message.py", line 1237, in _verify_expression_types
    proof = self._prove_path_property(expr.TRUE, p)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/model/message.py", line 1913, in _prove_path_property
    return prop.check([*self.type_constraints(prop), *conditions, *sizes])
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/expression.py", line 266, in check
    return Proof(self, facts)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/rflx/expression.py", line 64, in __init__
    solver.add(f.z3expr())
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/.venv/lib/python3.8/site-packages/z3/z3.py", line 7028, in add
    self.assert_exprs(*args)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/.venv/lib/python3.8/site-packages/z3/z3.py", line 7017, in assert_exprs
    Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/.venv/lib/python3.8/site-packages/z3/z3core.py", line 3951, in Z3_solver_assert
    _elems.Check(a0)
  File "/home/senier/Devel/RecordFlux_issue_review-2022-08-24/.venv/lib/python3.8/site-packages/z3/z3core.py", line 1475, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'invalid argument'

----------------------------------------------------------------------------

A bug was detected. Please report this issue on GitHub:

https://github.com/Componolit/RecordFlux/issues/new?labels=bug

Include the complete content of the bug box shown above and all input files
in the report.

The same happens if True is replaced by any other name. This should be rejected altogether (statically True conditions can just be left out) with a clean error message.