check_ast_bc.cpp

#include "ast.h"
#include "ast_gen.h"
#include "parser.h"

void check_ast_bc(size_t& good, size_t& bad) {
    AstGen::Gen const
        x = Ast::Identifier("x"),
        y = Ast::Identifier("y"),
        z = Ast::Identifier("z");

#define CHECK_AST(expr, ast) ++(Parser::check_ast(expr, ast)?good:bad)

#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wlogical-not-parentheses"
#pragma GCC diagnostic ignored "-Wparentheses"
    CHECK_AST(" +(x)< -y>= +z",  +(x)< -y>= +z);
    CHECK_AST(" +(x< -y)>= +z",  +(x< -y)>= +z);
    CHECK_AST(" +x<( -y)>= +z",  +x<( -y)>= +z);
    CHECK_AST(" +x< -(y)>= +z",  +x< -(y)>= +z);
    CHECK_AST("( +x)< -y>= -z", ( +x)< -y>= -z);
    CHECK_AST("( +x< -y)>= -z", ( +x< -y)>= -z);
    CHECK_AST(" +(x)< -y>= -z",  +(x)< -y>= -z);
    CHECK_AST(" +(x< -y)>= -z",  +(x< -y)>= -z);
    CHECK_AST(" +x<( -y)>= -z",  +x<( -y)>= -z);
    CHECK_AST(" +x< -(y)>= -z",  +x< -(y)>= -z);
    CHECK_AST("( +x)< -y>= not z", ( +x)< -y>= not z);
    CHECK_AST("( +x< -y)>= not z", ( +x< -y)>= not z);
    CHECK_AST(" +(x)< -y>= not z",  +(x)< -y>= not z);
    CHECK_AST(" +(x< -y)>= not z",  +(x< -y)>= not z);
    CHECK_AST(" +x<( -y)>= not z",  +x<( -y)>= not z);
    CHECK_AST(" +x< -(y)>= not z",  +x< -(y)>= not z);
    CHECK_AST("( +x)< not y>=z", ( +x)< not y>=z);
    CHECK_AST("( +x< not y)>=z", ( +x< not y)>=z);
    CHECK_AST(" +(x)< not y>=z",  +(x)< not y>=z);
    CHECK_AST(" +(x< not y)>=z",  +(x< not y)>=z);
    CHECK_AST(" +x<( not y)>=z",  +x<( not y)>=z);
    CHECK_AST(" +x< not (y)>=z",  +x< not (y)>=z);
    CHECK_AST("( +x)< not y>= +z", ( +x)< not y>= +z);
    CHECK_AST("( +x< not y)>= +z", ( +x< not y)>= +z);
    CHECK_AST(" +(x)< not y>= +z",  +(x)< not y>= +z);
    CHECK_AST(" +(x< not y)>= +z",  +(x< not y)>= +z);
    CHECK_AST(" +x<( not y)>= +z",  +x<( not y)>= +z);
    CHECK_AST(" +x< not (y)>= +z",  +x< not (y)>= +z);
    CHECK_AST("( +x)< not y>= -z", ( +x)< not y>= -z);
    CHECK_AST("( +x< not y)>= -z", ( +x< not y)>= -z);
    CHECK_AST(" +(x)< not y>= -z",  +(x)< not y>= -z);
    CHECK_AST(" +(x< not y)>= -z",  +(x< not y)>= -z);
    CHECK_AST(" +x<( not y)>= -z",  +x<( not y)>= -z);
    CHECK_AST(" +x< not (y)>= -z",  +x< not (y)>= -z);
    CHECK_AST("( +x)< not y>= not z", ( +x)< not y>= not z);
    CHECK_AST("( +x< not y)>= not z", ( +x< not y)>= not z);
    CHECK_AST(" +(x)< not y>= not z",  +(x)< not y>= not z);
    CHECK_AST(" +(x< not y)>= not z",  +(x< not y)>= not z);
    CHECK_AST(" +x<( not y)>= not z",  +x<( not y)>= not z);
    CHECK_AST(" +x< not (y)>= not z",  +x< not (y)>= not z);
    CHECK_AST("( -x)<y>=z", ( -x)<y>=z);
    CHECK_AST("( -x<y)>=z", ( -x<y)>=z);
    CHECK_AST(" -(x)<y>=z",  -(x)<y>=z);
    CHECK_AST(" -(x<y)>=z",  -(x<y)>=z);
    CHECK_AST(" -x<(y)>=z",  -x<(y)>=z);
    CHECK_AST("( -x)<y>= +z", ( -x)<y>= +z);
    CHECK_AST("( -x<y)>= +z", ( -x<y)>= +z);
    CHECK_AST(" -(x)<y>= +z",  -(x)<y>= +z);
    CHECK_AST(" -(x<y)>= +z",  -(x<y)>= +z);
    CHECK_AST(" -x<(y)>= +z",  -x<(y)>= +z);
    CHECK_AST("( -x)<y>= -z", ( -x)<y>= -z);
    CHECK_AST("( -x<y)>= -z", ( -x<y)>= -z);
    CHECK_AST(" -(x)<y>= -z",  -(x)<y>= -z);
    CHECK_AST(" -(x<y)>= -z",  -(x<y)>= -z);
    CHECK_AST(" -x<(y)>= -z",  -x<(y)>= -z);
    CHECK_AST("( -x)<y>= not z", ( -x)<y>= not z);
    CHECK_AST("( -x<y)>= not z", ( -x<y)>= not z);
    CHECK_AST(" -(x)<y>= not z",  -(x)<y>= not z);
    CHECK_AST(" -(x<y)>= not z",  -(x<y)>= not z);
    CHECK_AST(" -x<(y)>= not z",  -x<(y)>= not z);
    CHECK_AST("( -x)< +y>=z", ( -x)< +y>=z);
    CHECK_AST("( -x< +y)>=z", ( -x< +y)>=z);
    CHECK_AST(" -(x)< +y>=z",  -(x)< +y>=z);
    CHECK_AST(" -(x< +y)>=z",  -(x< +y)>=z);
    CHECK_AST(" -x<( +y)>=z",  -x<( +y)>=z);
    CHECK_AST(" -x< +(y)>=z",  -x< +(y)>=z);
    CHECK_AST("( -x)< +y>= +z", ( -x)< +y>= +z);
    CHECK_AST("( -x< +y)>= +z", ( -x< +y)>= +z);
    CHECK_AST(" -(x)< +y>= +z",  -(x)< +y>= +z);
    CHECK_AST(" -(x< +y)>= +z",  -(x< +y)>= +z);
    CHECK_AST(" -x<( +y)>= +z",  -x<( +y)>= +z);
    CHECK_AST(" -x< +(y)>= +z",  -x< +(y)>= +z);
    CHECK_AST("( -x)< +y>= -z", ( -x)< +y>= -z);
    CHECK_AST("( -x< +y)>= -z", ( -x< +y)>= -z);
    CHECK_AST(" -(x)< +y>= -z",  -(x)< +y>= -z);
    CHECK_AST(" -(x< +y)>= -z",  -(x< +y)>= -z);
    CHECK_AST(" -x<( +y)>= -z",  -x<( +y)>= -z);
    CHECK_AST(" -x< +(y)>= -z",  -x< +(y)>= -z);
    CHECK_AST("( -x)< +y>= not z", ( -x)< +y>= not z);
    CHECK_AST("( -x< +y)>= not z", ( -x< +y)>= not z);
    CHECK_AST(" -(x)< +y>= not z",  -(x)< +y>= not z);
    CHECK_AST(" -(x< +y)>= not z",  -(x< +y)>= not z);
    CHECK_AST(" -x<( +y)>= not z",  -x<( +y)>= not z);
    CHECK_AST(" -x< +(y)>= not z",  -x< +(y)>= not z);
    CHECK_AST("( -x)< -y>=z", ( -x)< -y>=z);
    CHECK_AST("( -x< -y)>=z", ( -x< -y)>=z);
    CHECK_AST(" -(x)< -y>=z",  -(x)< -y>=z);
    CHECK_AST(" -(x< -y)>=z",  -(x< -y)>=z);
    CHECK_AST(" -x<( -y)>=z",  -x<( -y)>=z);
    CHECK_AST(" -x< -(y)>=z",  -x< -(y)>=z);
    CHECK_AST("( -x)< -y>= +z", ( -x)< -y>= +z);
    CHECK_AST("( -x< -y)>= +z", ( -x< -y)>= +z);
    CHECK_AST(" -(x)< -y>= +z",  -(x)< -y>= +z);
    CHECK_AST(" -(x< -y)>= +z",  -(x< -y)>= +z);
    CHECK_AST(" -x<( -y)>= +z",  -x<( -y)>= +z);
    CHECK_AST(" -x< -(y)>= +z",  -x< -(y)>= +z);
    CHECK_AST("( -x)< -y>= -z", ( -x)< -y>= -z);
    CHECK_AST("( -x< -y)>= -z", ( -x< -y)>= -z);
    CHECK_AST(" -(x)< -y>= -z",  -(x)< -y>= -z);
    CHECK_AST(" -(x< -y)>= -z",  -(x< -y)>= -z);
    CHECK_AST(" -x<( -y)>= -z",  -x<( -y)>= -z);
    CHECK_AST(" -x< -(y)>= -z",  -x< -(y)>= -z);
    CHECK_AST("( -x)< -y>= not z", ( -x)< -y>= not z);
    CHECK_AST("( -x< -y)>= not z", ( -x< -y)>= not z);
    CHECK_AST(" -(x)< -y>= not z",  -(x)< -y>= not z);
    CHECK_AST(" -(x< -y)>= not z",  -(x< -y)>= not z);
    CHECK_AST(" -x<( -y)>= not z",  -x<( -y)>= not z);
    CHECK_AST(" -x< -(y)>= not z",  -x< -(y)>= not z);
    CHECK_AST("( -x)< not y>=z", ( -x)< not y>=z);
    CHECK_AST("( -x< not y)>=z", ( -x< not y)>=z);
    CHECK_AST(" -(x)< not y>=z",  -(x)< not y>=z);
    CHECK_AST(" -(x< not y)>=z",  -(x< not y)>=z);
    CHECK_AST(" -x<( not y)>=z",  -x<( not y)>=z);
    CHECK_AST(" -x< not (y)>=z",  -x< not (y)>=z);
    CHECK_AST("( -x)< not y>= +z", ( -x)< not y>= +z);
    CHECK_AST("( -x< not y)>= +z", ( -x< not y)>= +z);
    CHECK_AST(" -(x)< not y>= +z",  -(x)< not y>= +z);
    CHECK_AST(" -(x< not y)>= +z",  -(x< not y)>= +z);
    CHECK_AST(" -x<( not y)>= +z",  -x<( not y)>= +z);
    CHECK_AST(" -x< not (y)>= +z",  -x< not (y)>= +z);
    CHECK_AST("( -x)< not y>= -z", ( -x)< not y>= -z);
    CHECK_AST("( -x< not y)>= -z", ( -x< not y)>= -z);
    CHECK_AST(" -(x)< not y>= -z",  -(x)< not y>= -z);
    CHECK_AST(" -(x< not y)>= -z",  -(x< not y)>= -z);
    CHECK_AST(" -x<( not y)>= -z",  -x<( not y)>= -z);
    CHECK_AST(" -x< not (y)>= -z",  -x< not (y)>= -z);
    CHECK_AST("( -x)< not y>= not z", ( -x)< not y>= not z);
    CHECK_AST("( -x< not y)>= not z", ( -x< not y)>= not z);
    CHECK_AST(" -(x)< not y>= not z",  -(x)< not y>= not z);
    CHECK_AST(" -(x< not y)>= not z",  -(x< not y)>= not z);
    CHECK_AST(" -x<( not y)>= not z",  -x<( not y)>= not z);
    CHECK_AST(" -x< not (y)>= not z",  -x< not (y)>= not z);
    CHECK_AST("( not x)<y>=z", ( not x)<y>=z);
    CHECK_AST("( not x<y)>=z", ( not x<y)>=z);
    CHECK_AST(" not (x)<y>=z",  not (x)<y>=z);
    CHECK_AST(" not (x<y)>=z",  not (x<y)>=z);
    CHECK_AST(" not x<(y)>=z",  not x<(y)>=z);
    CHECK_AST("( not x)<y>= +z", ( not x)<y>= +z);
    CHECK_AST("( not x<y)>= +z", ( not x<y)>= +z);
    CHECK_AST(" not (x)<y>= +z",  not (x)<y>= +z);
    CHECK_AST(" not (x<y)>= +z",  not (x<y)>= +z);
    CHECK_AST(" not x<(y)>= +z",  not x<(y)>= +z);
    CHECK_AST("( not x)<y>= -z", ( not x)<y>= -z);
    CHECK_AST("( not x<y)>= -z", ( not x<y)>= -z);
    CHECK_AST(" not (x)<y>= -z",  not (x)<y>= -z);
    CHECK_AST(" not (x<y)>= -z",  not (x<y)>= -z);
    CHECK_AST(" not x<(y)>= -z",  not x<(y)>= -z);
    CHECK_AST("( not x)<y>= not z", ( not x)<y>= not z);
    CHECK_AST("( not x<y)>= not z", ( not x<y)>= not z);
    CHECK_AST(" not (x)<y>= not z",  not (x)<y>= not z);
    CHECK_AST(" not (x<y)>= not z",  not (x<y)>= not z);
    CHECK_AST(" not x<(y)>= not z",  not x<(y)>= not z);
    CHECK_AST("( not x)< +y>=z", ( not x)< +y>=z);
    CHECK_AST("( not x< +y)>=z", ( not x< +y)>=z);
    CHECK_AST(" not (x)< +y>=z",  not (x)< +y>=z);
    CHECK_AST(" not (x< +y)>=z",  not (x< +y)>=z);
    CHECK_AST(" not x<( +y)>=z",  not x<( +y)>=z);
    CHECK_AST(" not x< +(y)>=z",  not x< +(y)>=z);
    CHECK_AST("( not x)< +y>= +z", ( not x)< +y>= +z);
    CHECK_AST("( not x< +y)>= +z", ( not x< +y)>= +z);
    CHECK_AST(" not (x)< +y>= +z",  not (x)< +y>= +z);
    CHECK_AST(" not (x< +y)>= +z",  not (x< +y)>= +z);
    CHECK_AST(" not x<( +y)>= +z",  not x<( +y)>= +z);
    CHECK_AST(" not x< +(y)>= +z",  not x< +(y)>= +z);
    CHECK_AST("( not x)< +y>= -z", ( not x)< +y>= -z);
    CHECK_AST("( not x< +y)>= -z", ( not x< +y)>= -z);
    CHECK_AST(" not (x)< +y>= -z",  not (x)< +y>= -z);
    CHECK_AST(" not (x< +y)>= -z",  not (x< +y)>= -z);
    CHECK_AST(" not x<( +y)>= -z",  not x<( +y)>= -z);
    CHECK_AST(" not x< +(y)>= -z",  not x< +(y)>= -z);
    CHECK_AST("( not x)< +y>= not z", ( not x)< +y>= not z);
    CHECK_AST("( not x< +y)>= not z", ( not x< +y)>= not z);
    CHECK_AST(" not (x)< +y>= not z",  not (x)< +y>= not z);
    CHECK_AST(" not (x< +y)>= not z",  not (x< +y)>= not z);
    CHECK_AST(" not x<( +y)>= not z",  not x<( +y)>= not z);
    CHECK_AST(" not x< +(y)>= not z",  not x< +(y)>= not z);
    CHECK_AST("( not x)< -y>=z", ( not x)< -y>=z);
    CHECK_AST("( not x< -y)>=z", ( not x< -y)>=z);
    CHECK_AST(" not (x)< -y>=z",  not (x)< -y>=z);
    CHECK_AST(" not (x< -y)>=z",  not (x< -y)>=z);
    CHECK_AST(" not x<( -y)>=z",  not x<( -y)>=z);
    CHECK_AST(" not x< -(y)>=z",  not x< -(y)>=z);
    CHECK_AST("( not x)< -y>= +z", ( not x)< -y>= +z);
    CHECK_AST("( not x< -y)>= +z", ( not x< -y)>= +z);
    CHECK_AST(" not (x)< -y>= +z",  not (x)< -y>= +z);
    CHECK_AST(" not (x< -y)>= +z",  not (x< -y)>= +z);
    CHECK_AST(" not x<( -y)>= +z",  not x<( -y)>= +z);
    CHECK_AST(" not x< -(y)>= +z",  not x< -(y)>= +z);
    CHECK_AST("( not x)< -y>= -z", ( not x)< -y>= -z);
    CHECK_AST("( not x< -y)>= -z", ( not x< -y)>= -z);
    CHECK_AST(" not (x)< -y>= -z",  not (x)< -y>= -z);
    CHECK_AST(" not (x< -y)>= -z",  not (x< -y)>= -z);
    CHECK_AST(" not x<( -y)>= -z",  not x<( -y)>= -z);
    CHECK_AST(" not x< -(y)>= -z",  not x< -(y)>= -z);
    CHECK_AST("( not x)< -y>= not z", ( not x)< -y>= not z);
    CHECK_AST("( not x< -y)>= not z", ( not x< -y)>= not z);
    CHECK_AST(" not (x)< -y>= not z",  not (x)< -y>= not z);
    CHECK_AST(" not (x< -y)>= not z",  not (x< -y)>= not z);
    CHECK_AST(" not x<( -y)>= not z",  not x<( -y)>= not z);
    CHECK_AST(" not x< -(y)>= not z",  not x< -(y)>= not z);
    CHECK_AST("( not x)< not y>=z", ( not x)< not y>=z);
    CHECK_AST("( not x< not y)>=z", ( not x< not y)>=z);
    CHECK_AST(" not (x)< not y>=z",  not (x)< not y>=z);
    CHECK_AST(" not (x< not y)>=z",  not (x< not y)>=z);
    CHECK_AST(" not x<( not y)>=z",  not x<( not y)>=z);
    CHECK_AST(" not x< not (y)>=z",  not x< not (y)>=z);
    CHECK_AST("( not x)< not y>= +z", ( not x)< not y>= +z);
    CHECK_AST("( not x< not y)>= +z", ( not x< not y)>= +z);
    CHECK_AST(" not (x)< not y>= +z",  not (x)< not y>= +z);
    CHECK_AST(" not (x< not y)>= +z",  not (x< not y)>= +z);
    CHECK_AST(" not x<( not y)>= +z",  not x<( not y)>= +z);
    CHECK_AST(" not x< not (y)>= +z",  not x< not (y)>= +z);
    CHECK_AST("( not x)< not y>= -z", ( not x)< not y>= -z);
    CHECK_AST("( not x< not y)>= -z", ( not x< not y)>= -z);
    CHECK_AST(" not (x)< not y>= -z",  not (x)< not y>= -z);
    CHECK_AST(" not (x< not y)>= -z",  not (x< not y)>= -z);
    CHECK_AST(" not x<( not y)>= -z",  not x<( not y)>= -z);
    CHECK_AST(" not x< not (y)>= -z",  not x< not (y)>= -z);
    CHECK_AST("( not x)< not y>= not z", ( not x)< not y>= not z);
    CHECK_AST("( not x< not y)>= not z", ( not x< not y)>= not z);
    CHECK_AST(" not (x)< not y>= not z",  not (x)< not y>= not z);
    CHECK_AST(" not (x< not y)>= not z",  not (x< not y)>= not z);
    CHECK_AST(" not x<( not y)>= not z",  not x<( not y)>= not z);
    CHECK_AST(" not x< not (y)>= not z",  not x< not (y)>= not z);
    CHECK_AST("(x)<y=z", (x)<y==z);
    CHECK_AST("(x<y)=z", (x<y)==z);
    CHECK_AST("x<(y)=z", x<(y)==z);
    CHECK_AST("(x)<y= +z", (x)<y== +z);
    CHECK_AST("(x<y)= +z", (x<y)== +z);
    CHECK_AST("x<(y)= +z", x<(y)== +z);
    CHECK_AST("(x)<y= -z", (x)<y== -z);
    CHECK_AST("(x<y)= -z", (x<y)== -z);
    CHECK_AST("x<(y)= -z", x<(y)== -z);
    CHECK_AST("(x)<y= not z", (x)<y== not z);
    CHECK_AST("(x<y)= not z", (x<y)== not z);
    CHECK_AST("x<(y)= not z", x<(y)== not z);
    CHECK_AST("(x)< +y=z", (x)< +y==z);
    CHECK_AST("(x< +y)=z", (x< +y)==z);
    CHECK_AST("x<( +y)=z", x<( +y)==z);
    CHECK_AST("x< +(y)=z", x< +(y)==z);
    CHECK_AST("(x)< +y= +z", (x)< +y== +z);
    CHECK_AST("(x< +y)= +z", (x< +y)== +z);
    CHECK_AST("x<( +y)= +z", x<( +y)== +z);
    CHECK_AST("x< +(y)= +z", x< +(y)== +z);
    CHECK_AST("(x)< +y= -z", (x)< +y== -z);
    CHECK_AST("(x< +y)= -z", (x< +y)== -z);
    CHECK_AST("x<( +y)= -z", x<( +y)== -z);
    CHECK_AST("x< +(y)= -z", x< +(y)== -z);
    CHECK_AST("(x)< +y= not z", (x)< +y== not z);
    CHECK_AST("(x< +y)= not z", (x< +y)== not z);
    CHECK_AST("x<( +y)= not z", x<( +y)== not z);
    CHECK_AST("x< +(y)= not z", x< +(y)== not z);
    CHECK_AST("(x)< -y=z", (x)< -y==z);
    CHECK_AST("(x< -y)=z", (x< -y)==z);
    CHECK_AST("x<( -y)=z", x<( -y)==z);
    CHECK_AST("x< -(y)=z", x< -(y)==z);
    CHECK_AST("(x)< -y= +z", (x)< -y== +z);
    CHECK_AST("(x< -y)= +z", (x< -y)== +z);
    CHECK_AST("x<( -y)= +z", x<( -y)== +z);
    CHECK_AST("x< -(y)= +z", x< -(y)== +z);
    CHECK_AST("(x)< -y= -z", (x)< -y== -z);
    CHECK_AST("(x< -y)= -z", (x< -y)== -z);
    CHECK_AST("x<( -y)= -z", x<( -y)== -z);
    CHECK_AST("x< -(y)= -z", x< -(y)== -z);
    CHECK_AST("(x)< -y= not z", (x)< -y== not z);
    CHECK_AST("(x< -y)= not z", (x< -y)== not z);
    CHECK_AST("x<( -y)= not z", x<( -y)== not z);
    CHECK_AST("x< -(y)= not z", x< -(y)== not z);
    CHECK_AST("(x)< not y=z", (x)< not y==z);
    CHECK_AST("(x< not y)=z", (x< not y)==z);
    CHECK_AST("x<( not y)=z", x<( not y)==z);
    CHECK_AST("x< not (y)=z", x< not (y)==z);
    CHECK_AST("(x)< not y= +z", (x)< not y== +z);
    CHECK_AST("(x< not y)= +z", (x< not y)== +z);
    CHECK_AST("x<( not y)= +z", x<( not y)== +z);
    CHECK_AST("x< not (y)= +z", x< not (y)== +z);
    CHECK_AST("(x)< not y= -z", (x)< not y== -z);
    CHECK_AST("(x< not y)= -z", (x< not y)== -z);
    CHECK_AST("x<( not y)= -z", x<( not y)== -z);
    CHECK_AST("x< not (y)= -z", x< not (y)== -z);
    CHECK_AST("(x)< not y= not z", (x)< not y== not z);
    CHECK_AST("(x< not y)= not z", (x< not y)== not z);
    CHECK_AST("x<( not y)= not z", x<( not y)== not z);
    CHECK_AST("x< not (y)= not z", x< not (y)== not z);
    CHECK_AST("( +x)<y=z", ( +x)<y==z);
    CHECK_AST("( +x<y)=z", ( +x<y)==z);
    CHECK_AST(" +(x)<y=z",  +(x)<y==z);
    CHECK_AST(" +(x<y)=z",  +(x<y)==z);
    CHECK_AST(" +x<(y)=z",  +x<(y)==z);
    CHECK_AST("( +x)<y= +z", ( +x)<y== +z);
    CHECK_AST("( +x<y)= +z", ( +x<y)== +z);
    CHECK_AST(" +(x)<y= +z",  +(x)<y== +z);
    CHECK_AST(" +(x<y)= +z",  +(x<y)== +z);
    CHECK_AST(" +x<(y)= +z",  +x<(y)== +z);
    CHECK_AST("( +x)<y= -z", ( +x)<y== -z);
    CHECK_AST("( +x<y)= -z", ( +x<y)== -z);
    CHECK_AST(" +(x)<y= -z",  +(x)<y== -z);
    CHECK_AST(" +(x<y)= -z",  +(x<y)== -z);
    CHECK_AST(" +x<(y)= -z",  +x<(y)== -z);
    CHECK_AST("( +x)<y= not z", ( +x)<y== not z);
    CHECK_AST("( +x<y)= not z", ( +x<y)== not z);
    CHECK_AST(" +(x)<y= not z",  +(x)<y== not z);
    CHECK_AST(" +(x<y)= not z",  +(x<y)== not z);
    CHECK_AST(" +x<(y)= not z",  +x<(y)== not z);
    CHECK_AST("( +x)< +y=z", ( +x)< +y==z);
    CHECK_AST("( +x< +y)=z", ( +x< +y)==z);
    CHECK_AST(" +(x)< +y=z",  +(x)< +y==z);
    CHECK_AST(" +(x< +y)=z",  +(x< +y)==z);
    CHECK_AST(" +x<( +y)=z",  +x<( +y)==z);
    CHECK_AST(" +x< +(y)=z",  +x< +(y)==z);
    CHECK_AST("( +x)< +y= +z", ( +x)< +y== +z);
    CHECK_AST("( +x< +y)= +z", ( +x< +y)== +z);
    CHECK_AST(" +(x)< +y= +z",  +(x)< +y== +z);
    CHECK_AST(" +(x< +y)= +z",  +(x< +y)== +z);
    CHECK_AST(" +x<( +y)= +z",  +x<( +y)== +z);
    CHECK_AST(" +x< +(y)= +z",  +x< +(y)== +z);
    CHECK_AST("( +x)< +y= -z", ( +x)< +y== -z);
    CHECK_AST("( +x< +y)= -z", ( +x< +y)== -z);
    CHECK_AST(" +(x)< +y= -z",  +(x)< +y== -z);
    CHECK_AST(" +(x< +y)= -z",  +(x< +y)== -z);
    CHECK_AST(" +x<( +y)= -z",  +x<( +y)== -z);
    CHECK_AST(" +x< +(y)= -z",  +x< +(y)== -z);
    CHECK_AST("( +x)< +y= not z", ( +x)< +y== not z);
    CHECK_AST("( +x< +y)= not z", ( +x< +y)== not z);
    CHECK_AST(" +(x)< +y= not z",  +(x)< +y== not z);
    CHECK_AST(" +(x< +y)= not z",  +(x< +y)== not z);
    CHECK_AST(" +x<( +y)= not z",  +x<( +y)== not z);
    CHECK_AST(" +x< +(y)= not z",  +x< +(y)== not z);
    CHECK_AST("( +x)< -y=z", ( +x)< -y==z);
    CHECK_AST("( +x< -y)=z", ( +x< -y)==z);
    CHECK_AST(" +(x)< -y=z",  +(x)< -y==z);
    CHECK_AST(" +(x< -y)=z",  +(x< -y)==z);
    CHECK_AST(" +x<( -y)=z",  +x<( -y)==z);
    CHECK_AST(" +x< -(y)=z",  +x< -(y)==z);
    CHECK_AST("( +x)< -y= +z", ( +x)< -y== +z);
    CHECK_AST("( +x< -y)= +z", ( +x< -y)== +z);
    CHECK_AST(" +(x)< -y= +z",  +(x)< -y== +z);
    CHECK_AST(" +(x< -y)= +z",  +(x< -y)== +z);
    CHECK_AST(" +x<( -y)= +z",  +x<( -y)== +z);
    CHECK_AST(" +x< -(y)= +z",  +x< -(y)== +z);
    CHECK_AST("( +x)< -y= -z", ( +x)< -y== -z);
    CHECK_AST("( +x< -y)= -z", ( +x< -y)== -z);
    CHECK_AST(" +(x)< -y= -z",  +(x)< -y== -z);
    CHECK_AST(" +(x< -y)= -z",  +(x< -y)== -z);
    CHECK_AST(" +x<( -y)= -z",  +x<( -y)== -z);
    CHECK_AST(" +x< -(y)= -z",  +x< -(y)== -z);
    CHECK_AST("( +x)< -y= not z", ( +x)< -y== not z);
    CHECK_AST("( +x< -y)= not z", ( +x< -y)== not z);
    CHECK_AST(" +(x)< -y= not z",  +(x)< -y== not z);
    CHECK_AST(" +(x< -y)= not z",  +(x< -y)== not z);
    CHECK_AST(" +x<( -y)= not z",  +x<( -y)== not z);
    CHECK_AST(" +x< -(y)= not z",  +x< -(y)== not z);
    CHECK_AST("( +x)< not y=z", ( +x)< not y==z);
    CHECK_AST("( +x< not y)=z", ( +x< not y)==z);
    CHECK_AST(" +(x)< not y=z",  +(x)< not y==z);
    CHECK_AST(" +(x< not y)=z",  +(x< not y)==z);
    CHECK_AST(" +x<( not y)=z",  +x<( not y)==z);
    CHECK_AST(" +x< not (y)=z",  +x< not (y)==z);
    CHECK_AST("( +x)< not y= +z", ( +x)< not y== +z);
    CHECK_AST("( +x< not y)= +z", ( +x< not y)== +z);
    CHECK_AST(" +(x)< not y= +z",  +(x)< not y== +z);
    CHECK_AST(" +(x< not y)= +z",  +(x< not y)== +z);
    CHECK_AST(" +x<( not y)= +z",  +x<( not y)== +z);
    CHECK_AST(" +x< not (y)= +z",  +x< not (y)== +z);
    CHECK_AST("( +x)< not y= -z", ( +x)< not y== -z);
    CHECK_AST("( +x< not y)= -z", ( +x< not y)== -z);
    CHECK_AST(" +(x)< not y= -z",  +(x)< not y== -z);
    CHECK_AST(" +(x< not y)= -z",  +(x< not y)== -z);
    CHECK_AST(" +x<( not y)= -z",  +x<( not y)== -z);
    CHECK_AST(" +x< not (y)= -z",  +x< not (y)== -z);
    CHECK_AST("( +x)< not y= not z", ( +x)< not y== not z);
    CHECK_AST("( +x< not y)= not z", ( +x< not y)== not z);
    CHECK_AST(" +(x)< not y= not z",  +(x)< not y== not z);
    CHECK_AST(" +(x< not y)= not z",  +(x< not y)== not z);
    CHECK_AST(" +x<( not y)= not z",  +x<( not y)== not z);
    CHECK_AST(" +x< not (y)= not z",  +x< not (y)== not z);
    CHECK_AST("( -x)<y=z", ( -x)<y==z);
    CHECK_AST("( -x<y)=z", ( -x<y)==z);
    CHECK_AST(" -(x)<y=z",  -(x)<y==z);
    CHECK_AST(" -(x<y)=z",  -(x<y)==z);
    CHECK_AST(" -x<(y)=z",  -x<(y)==z);
    CHECK_AST("( -x)<y= +z", ( -x)<y== +z);
    CHECK_AST("( -x<y)= +z", ( -x<y)== +z);
    CHECK_AST(" -(x)<y= +z",  -(x)<y== +z);
    CHECK_AST(" -(x<y)= +z",  -(x<y)== +z);
    CHECK_AST(" -x<(y)= +z",  -x<(y)== +z);
    CHECK_AST("( -x)<y= -z", ( -x)<y== -z);
    CHECK_AST("( -x<y)= -z", ( -x<y)== -z);
    CHECK_AST(" -(x)<y= -z",  -(x)<y== -z);
    CHECK_AST(" -(x<y)= -z",  -(x<y)== -z);
    CHECK_AST(" -x<(y)= -z",  -x<(y)== -z);
    CHECK_AST("( -x)<y= not z", ( -x)<y== not z);
    CHECK_AST("( -x<y)= not z", ( -x<y)== not z);
    CHECK_AST(" -(x)<y= not z",  -(x)<y== not z);
    CHECK_AST(" -(x<y)= not z",  -(x<y)== not z);
    CHECK_AST(" -x<(y)= not z",  -x<(y)== not z);
    CHECK_AST("( -x)< +y=z", ( -x)< +y==z);
    CHECK_AST("( -x< +y)=z", ( -x< +y)==z);
    CHECK_AST(" -(x)< +y=z",  -(x)< +y==z);
    CHECK_AST(" -(x< +y)=z",  -(x< +y)==z);
    CHECK_AST(" -x<( +y)=z",  -x<( +y)==z);
    CHECK_AST(" -x< +(y)=z",  -x< +(y)==z);
    CHECK_AST("( -x)< +y= +z", ( -x)< +y== +z);
    CHECK_AST("( -x< +y)= +z", ( -x< +y)== +z);
    CHECK_AST(" -(x)< +y= +z",  -(x)< +y== +z);
    CHECK_AST(" -(x< +y)= +z",  -(x< +y)== +z);
    CHECK_AST(" -x<( +y)= +z",  -x<( +y)== +z);
    CHECK_AST(" -x< +(y)= +z",  -x< +(y)== +z);
    CHECK_AST("( -x)< +y= -z", ( -x)< +y== -z);
    CHECK_AST("( -x< +y)= -z", ( -x< +y)== -z);
    CHECK_AST(" -(x)< +y= -z",  -(x)< +y== -z);
    CHECK_AST(" -(x< +y)= -z",  -(x< +y)== -z);
    CHECK_AST(" -x<( +y)= -z",  -x<( +y)== -z);
    CHECK_AST(" -x< +(y)= -z",  -x< +(y)== -z);
    CHECK_AST("( -x)< +y= not z", ( -x)< +y== not z);
    CHECK_AST("( -x< +y)= not z", ( -x< +y)== not z);
    CHECK_AST(" -(x)< +y= not z",  -(x)< +y== not z);
    CHECK_AST(" -(x< +y)= not z",  -(x< +y)== not z);
    CHECK_AST(" -x<( +y)= not z",  -x<( +y)== not z);
    CHECK_AST(" -x< +(y)= not z",  -x< +(y)== not z);
    CHECK_AST("( -x)< -y=z", ( -x)< -y==z);
    CHECK_AST("( -x< -y)=z", ( -x< -y)==z);
    CHECK_AST(" -(x)< -y=z",  -(x)< -y==z);
    CHECK_AST(" -(x< -y)=z",  -(x< -y)==z);
    CHECK_AST(" -x<( -y)=z",  -x<( -y)==z);
    CHECK_AST(" -x< -(y)=z",  -x< -(y)==z);
    CHECK_AST("( -x)< -y= +z", ( -x)< -y== +z);
    CHECK_AST("( -x< -y)= +z", ( -x< -y)== +z);
    CHECK_AST(" -(x)< -y= +z",  -(x)< -y== +z);
    CHECK_AST(" -(x< -y)= +z",  -(x< -y)== +z);
    CHECK_AST(" -x<( -y)= +z",  -x<( -y)== +z);
    CHECK_AST(" -x< -(y)= +z",  -x< -(y)== +z);
    CHECK_AST("( -x)< -y= -z", ( -x)< -y== -z);
    CHECK_AST("( -x< -y)= -z", ( -x< -y)== -z);
    CHECK_AST(" -(x)< -y= -z",  -(x)< -y== -z);
    CHECK_AST(" -(x< -y)= -z",  -(x< -y)== -z);
    CHECK_AST(" -x<( -y)= -z",  -x<( -y)== -z);
    CHECK_AST(" -x< -(y)= -z",  -x< -(y)== -z);
    CHECK_AST("( -x)< -y= not z", ( -x)< -y== not z);
    CHECK_AST("( -x< -y)= not z", ( -x< -y)== not z);
    CHECK_AST(" -(x)< -y= not z",  -(x)< -y== not z);
    CHECK_AST(" -(x< -y)= not z",  -(x< -y)== not z);
    CHECK_AST(" -x<( -y)= not z",  -x<( -y)== not z);
    CHECK_AST(" -x< -(y)= not z",  -x< -(y)== not z);
    CHECK_AST("( -x)< not y=z", ( -x)< not y==z);
    CHECK_AST("( -x< not y)=z", ( -x< not y)==z);
    CHECK_AST(" -(x)< not y=z",  -(x)< not y==z);
    CHECK_AST(" -(x< not y)=z",  -(x< not y)==z);
    CHECK_AST(" -x<( not y)=z",  -x<( not y)==z);
    CHECK_AST(" -x< not (y)=z",  -x< not (y)==z);
    CHECK_AST("( -x)< not y= +z", ( -x)< not y== +z);
    CHECK_AST("( -x< not y)= +z", ( -x< not y)== +z);
    CHECK_AST(" -(x)< not y= +z",  -(x)< not y== +z);
    CHECK_AST(" -(x< not y)= +z",  -(x< not y)== +z);
    CHECK_AST(" -x<( not y)= +z",  -x<( not y)== +z);
    CHECK_AST(" -x< not (y)= +z",  -x< not (y)== +z);
    CHECK_AST("( -x)< not y= -z", ( -x)< not y== -z);
    CHECK_AST("( -x< not y)= -z", ( -x< not y)== -z);
    CHECK_AST(" -(x)< not y= -z",  -(x)< not y== -z);
    CHECK_AST(" -(x< not y)= -z",  -(x< not y)== -z);
    CHECK_AST(" -x<( not y)= -z",  -x<( not y)== -z);
    CHECK_AST(" -x< not (y)= -z",  -x< not (y)== -z);
    CHECK_AST("( -x)< not y= not z", ( -x)< not y== not z);
    CHECK_AST("( -x< not y)= not z", ( -x< not y)== not z);
    CHECK_AST(" -(x)< not y= not z",  -(x)< not y== not z);
    CHECK_AST(" -(x< not y)= not z",  -(x< not y)== not z);
    CHECK_AST(" -x<( not y)= not z",  -x<( not y)== not z);
    CHECK_AST(" -x< not (y)= not z",  -x< not (y)== not z);
    CHECK_AST("( not x)<y=z", ( not x)<y==z);
    CHECK_AST("( not x<y)=z", ( not x<y)==z);
    CHECK_AST(" not (x)<y=z",  not (x)<y==z);
    CHECK_AST(" not (x<y)=z",  not (x<y)==z);
    CHECK_AST(" not x<(y)=z",  not x<(y)==z);
    CHECK_AST("( not x)<y= +z", ( not x)<y== +z);
    CHECK_AST("( not x<y)= +z", ( not x<y)== +z);
    CHECK_AST(" not (x)<y= +z",  not (x)<y== +z);
    CHECK_AST(" not (x<y)= +z",  not (x<y)== +z);
    CHECK_AST(" not x<(y)= +z",  not x<(y)== +z);
    CHECK_AST("( not x)<y= -z", ( not x)<y== -z);
    CHECK_AST("( not x<y)= -z", ( not x<y)== -z);
    CHECK_AST(" not (x)<y= -z",  not (x)<y== -z);
    CHECK_AST(" not (x<y)= -z",  not (x<y)== -z);
    CHECK_AST(" not x<(y)= -z",  not x<(y)== -z);
    CHECK_AST("( not x)<y= not z", ( not x)<y== not z);
    CHECK_AST("( not x<y)= not z", ( not x<y)== not z);
    CHECK_AST(" not (x)<y= not z",  not (x)<y== not z);
    CHECK_AST(" not (x<y)= not z",  not (x<y)== not z);
    CHECK_AST(" not x<(y)= not z",  not x<(y)== not z);
    CHECK_AST("( not x)< +y=z", ( not x)< +y==z);
    CHECK_AST("( not x< +y)=z", ( not x< +y)==z);
    CHECK_AST(" not (x)< +y=z",  not (x)< +y==z);
    CHECK_AST(" not (x< +y)=z",  not (x< +y)==z);
    CHECK_AST(" not x<( +y)=z",  not x<( +y)==z);
    CHECK_AST(" not x< +(y)=z",  not x< +(y)==z);
    CHECK_AST("( not x)< +y= +z", ( not x)< +y== +z);
    CHECK_AST("( not x< +y)= +z", ( not x< +y)== +z);
    CHECK_AST(" not (x)< +y= +z",  not (x)< +y== +z);
    CHECK_AST(" not (x< +y)= +z",  not (x< +y)== +z);
    CHECK_AST(" not x<( +y)= +z",  not x<( +y)== +z);
    CHECK_AST(" not x< +(y)= +z",  not x< +(y)== +z);
    CHECK_AST("( not x)< +y= -z", ( not x)< +y== -z);
    CHECK_AST("( not x< +y)= -z", ( not x< +y)== -z);
    CHECK_AST(" not (x)< +y= -z",  not (x)< +y== -z);
    CHECK_AST(" not (x< +y)= -z",  not (x< +y)== -z);
    CHECK_AST(" not x<( +y)= -z",  not x<( +y)== -z);
    CHECK_AST(" not x< +(y)= -z",  not x< +(y)== -z);
    CHECK_AST("( not x)< +y= not z", ( not x)< +y== not z);
    CHECK_AST("( not x< +y)= not z", ( not x< +y)== not z);
    CHECK_AST(" not (x)< +y= not z",  not (x)< +y== not z);
    CHECK_AST(" not (x< +y)= not z",  not (x< +y)== not z);
    CHECK_AST(" not x<( +y)= not z",  not x<( +y)== not z);
    CHECK_AST(" not x< +(y)= not z",  not x< +(y)== not z);
    CHECK_AST("( not x)< -y=z", ( not x)< -y==z);
    CHECK_AST("( not x< -y)=z", ( not x< -y)==z);
    CHECK_AST(" not (x)< -y=z",  not (x)< -y==z);
    CHECK_AST(" not (x< -y)=z",  not (x< -y)==z);
    CHECK_AST(" not x<( -y)=z",  not x<( -y)==z);
    CHECK_AST(" not x< -(y)=z",  not x< -(y)==z);
    CHECK_AST("( not x)< -y= +z", ( not x)< -y== +z);
    CHECK_AST("( not x< -y)= +z", ( not x< -y)== +z);
    CHECK_AST(" not (x)< -y= +z",  not (x)< -y== +z);
    CHECK_AST(" not (x< -y)= +z",  not (x< -y)== +z);
    CHECK_AST(" not x<( -y)= +z",  not x<( -y)== +z);
    CHECK_AST(" not x< -(y)= +z",  not x< -(y)== +z);
    CHECK_AST("( not x)< -y= -z", ( not x)< -y== -z);
    CHECK_AST("( not x< -y)= -z", ( not x< -y)== -z);
    CHECK_AST(" not (x)< -y= -z",  not (x)< -y== -z);
    CHECK_AST(" not (x< -y)= -z",  not (x< -y)== -z);
    CHECK_AST(" not x<( -y)= -z",  not x<( -y)== -z);
    CHECK_AST(" not x< -(y)= -z",  not x< -(y)== -z);
    CHECK_AST("( not x)< -y= not z", ( not x)< -y== not z);
    CHECK_AST("( not x< -y)= not z", ( not x< -y)== not z);
    CHECK_AST(" not (x)< -y= not z",  not (x)< -y== not z);
    CHECK_AST(" not (x< -y)= not z",  not (x< -y)== not z);
    CHECK_AST(" not x<( -y)= not z",  not x<( -y)== not z);
    CHECK_AST(" not x< -(y)= not z",  not x< -(y)== not z);
    CHECK_AST("( not x)< not y=z", ( not x)< not y==z);
    CHECK_AST("( not x< not y)=z", ( not x< not y)==z);
    CHECK_AST(" not (x)< not y=z",  not (x)< not y==z);
    CHECK_AST(" not (x< not y)=z",  not (x< not y)==z);
    CHECK_AST(" not x<( not y)=z",  not x<( not y)==z);
    CHECK_AST(" not x< not (y)=z",  not x< not (y)==z);
    CHECK_AST("( not x)< not y= +z", ( not x)< not y== +z);
    CHECK_AST("( not x< not y)= +z", ( not x< not y)== +z);
    CHECK_AST(" not (x)< not y= +z",  not (x)< not y== +z);
    CHECK_AST(" not (x< not y)= +z",  not (x< not y)== +z);
    CHECK_AST(" not x<( not y)= +z",  not x<( not y)== +z);
    CHECK_AST(" not x< not (y)= +z",  not x< not (y)== +z);
    CHECK_AST("( not x)< not y= -z", ( not x)< not y== -z);
    CHECK_AST("( not x< not y)= -z", ( not x< not y)== -z);
    CHECK_AST(" not (x)< not y= -z",  not (x)< not y== -z);
    CHECK_AST(" not (x< not y)= -z",  not (x< not y)== -z);
    CHECK_AST(" not x<( not y)= -z",  not x<( not y)== -z);
    CHECK_AST(" not x< not (y)= -z",  not x< not (y)== -z);
    CHECK_AST("( not x)< not y= not z", ( not x)< not y== not z);
    CHECK_AST("( not x< not y)= not z", ( not x< not y)== not z);
    CHECK_AST(" not (x)< not y= not z",  not (x)< not y== not z);
    CHECK_AST(" not (x< not y)= not z",  not (x< not y)== not z);
    CHECK_AST(" not x<( not y)= not z",  not x<( not y)== not z);
    CHECK_AST(" not x< not (y)= not z",  not x< not (y)== not z);
    CHECK_AST("(x)<y<>z", (x)<y!=z);
    CHECK_AST("(x<y)<>z", (x<y)!=z);
    CHECK_AST("x<(y)<>z", x<(y)!=z);
    CHECK_AST("(x)<y<> +z", (x)<y!= +z);
    CHECK_AST("(x<y)<> +z", (x<y)!= +z);
    CHECK_AST("x<(y)<> +z", x<(y)!= +z);
    CHECK_AST("(x)<y<> -z", (x)<y!= -z);
    CHECK_AST("(x<y)<> -z", (x<y)!= -z);
    CHECK_AST("x<(y)<> -z", x<(y)!= -z);
    CHECK_AST("(x)<y<> not z", (x)<y!= not z);
    CHECK_AST("(x<y)<> not z", (x<y)!= not z);
    CHECK_AST("x<(y)<> not z", x<(y)!= not z);
    CHECK_AST("(x)< +y<>z", (x)< +y!=z);
    CHECK_AST("(x< +y)<>z", (x< +y)!=z);
    CHECK_AST("x<( +y)<>z", x<( +y)!=z);
    CHECK_AST("x< +(y)<>z", x< +(y)!=z);
    CHECK_AST("(x)< +y<> +z", (x)< +y!= +z);
    CHECK_AST("(x< +y)<> +z", (x< +y)!= +z);
    CHECK_AST("x<( +y)<> +z", x<( +y)!= +z);
    CHECK_AST("x< +(y)<> +z", x< +(y)!= +z);
    CHECK_AST("(x)< +y<> -z", (x)< +y!= -z);
    CHECK_AST("(x< +y)<> -z", (x< +y)!= -z);
    CHECK_AST("x<( +y)<> -z", x<( +y)!= -z);
    CHECK_AST("x< +(y)<> -z", x< +(y)!= -z);
    CHECK_AST("(x)< +y<> not z", (x)< +y!= not z);
    CHECK_AST("(x< +y)<> not z", (x< +y)!= not z);
    CHECK_AST("x<( +y)<> not z", x<( +y)!= not z);
    CHECK_AST("x< +(y)<> not z", x< +(y)!= not z);
    CHECK_AST("(x)< -y<>z", (x)< -y!=z);
    CHECK_AST("(x< -y)<>z", (x< -y)!=z);
    CHECK_AST("x<( -y)<>z", x<( -y)!=z);
    CHECK_AST("x< -(y)<>z", x< -(y)!=z);
    CHECK_AST("(x)< -y<> +z", (x)< -y!= +z);
    CHECK_AST("(x< -y)<> +z", (x< -y)!= +z);
    CHECK_AST("x<( -y)<> +z", x<( -y)!= +z);
    CHECK_AST("x< -(y)<> +z", x< -(y)!= +z);
    CHECK_AST("(x)< -y<> -z", (x)< -y!= -z);
    CHECK_AST("(x< -y)<> -z", (x< -y)!= -z);
    CHECK_AST("x<( -y)<> -z", x<( -y)!= -z);
    CHECK_AST("x< -(y)<> -z", x< -(y)!= -z);
    CHECK_AST("(x)< -y<> not z", (x)< -y!= not z);
    CHECK_AST("(x< -y)<> not z", (x< -y)!= not z);
    CHECK_AST("x<( -y)<> not z", x<( -y)!= not z);
    CHECK_AST("x< -(y)<> not z", x< -(y)!= not z);
    CHECK_AST("(x)< not y<>z", (x)< not y!=z);
    CHECK_AST("(x< not y)<>z", (x< not y)!=z);
    CHECK_AST("x<( not y)<>z", x<( not y)!=z);
    CHECK_AST("x< not (y)<>z", x< not (y)!=z);
    CHECK_AST("(x)< not y<> +z", (x)< not y!= +z);
    CHECK_AST("(x< not y)<> +z", (x< not y)!= +z);
    CHECK_AST("x<( not y)<> +z", x<( not y)!= +z);
    CHECK_AST("x< not (y)<> +z", x< not (y)!= +z);
    CHECK_AST("(x)< not y<> -z", (x)< not y!= -z);
    CHECK_AST("(x< not y)<> -z", (x< not y)!= -z);
    CHECK_AST("x<( not y)<> -z", x<( not y)!= -z);
    CHECK_AST("x< not (y)<> -z", x< not (y)!= -z);
    CHECK_AST("(x)< not y<> not z", (x)< not y!= not z);
    CHECK_AST("(x< not y)<> not z", (x< not y)!= not z);
    CHECK_AST("x<( not y)<> not z", x<( not y)!= not z);
    CHECK_AST("x< not (y)<> not z", x< not (y)!= not z);
    CHECK_AST("( +x)<y<>z", ( +x)<y!=z);
    CHECK_AST("( +x<y)<>z", ( +x<y)!=z);
    CHECK_AST(" +(x)<y<>z",  +(x)<y!=z);
    CHECK_AST(" +(x<y)<>z",  +(x<y)!=z);
    CHECK_AST(" +x<(y)<>z",  +x<(y)!=z);
    CHECK_AST("( +x)<y<> +z", ( +x)<y!= +z);
    CHECK_AST("( +x<y)<> +z", ( +x<y)!= +z);
    CHECK_AST(" +(x)<y<> +z",  +(x)<y!= +z);
    CHECK_AST(" +(x<y)<> +z",  +(x<y)!= +z);
    CHECK_AST(" +x<(y)<> +z",  +x<(y)!= +z);
    CHECK_AST("( +x)<y<> -z", ( +x)<y!= -z);
    CHECK_AST("( +x<y)<> -z", ( +x<y)!= -z);
    CHECK_AST(" +(x)<y<> -z",  +(x)<y!= -z);
    CHECK_AST(" +(x<y)<> -z",  +(x<y)!= -z);
    CHECK_AST(" +x<(y)<> -z",  +x<(y)!= -z);
    CHECK_AST("( +x)<y<> not z", ( +x)<y!= not z);
    CHECK_AST("( +x<y)<> not z", ( +x<y)!= not z);
    CHECK_AST(" +(x)<y<> not z",  +(x)<y!= not z);
    CHECK_AST(" +(x<y)<> not z",  +(x<y)!= not z);
    CHECK_AST(" +x<(y)<> not z",  +x<(y)!= not z);
    CHECK_AST("( +x)< +y<>z", ( +x)< +y!=z);
    CHECK_AST("( +x< +y)<>z", ( +x< +y)!=z);
    CHECK_AST(" +(x)< +y<>z",  +(x)< +y!=z);
    CHECK_AST(" +(x< +y)<>z",  +(x< +y)!=z);
    CHECK_AST(" +x<( +y)<>z",  +x<( +y)!=z);
    CHECK_AST(" +x< +(y)<>z",  +x< +(y)!=z);
    CHECK_AST("( +x)< +y<> +z", ( +x)< +y!= +z);
    CHECK_AST("( +x< +y)<> +z", ( +x< +y)!= +z);
    CHECK_AST(" +(x)< +y<> +z",  +(x)< +y!= +z);
    CHECK_AST(" +(x< +y)<> +z",  +(x< +y)!= +z);
    CHECK_AST(" +x<( +y)<> +z",  +x<( +y)!= +z);
    CHECK_AST(" +x< +(y)<> +z",  +x< +(y)!= +z);
    CHECK_AST("( +x)< +y<> -z", ( +x)< +y!= -z);
    CHECK_AST("( +x< +y)<> -z", ( +x< +y)!= -z);
    CHECK_AST(" +(x)< +y<> -z",  +(x)< +y!= -z);
    CHECK_AST(" +(x< +y)<> -z",  +(x< +y)!= -z);
    CHECK_AST(" +x<( +y)<> -z",  +x<( +y)!= -z);
    CHECK_AST(" +x< +(y)<> -z",  +x< +(y)!= -z);
    CHECK_AST("( +x)< +y<> not z", ( +x)< +y!= not z);
    CHECK_AST("( +x< +y)<> not z", ( +x< +y)!= not z);
    CHECK_AST(" +(x)< +y<> not z",  +(x)< +y!= not z);
    CHECK_AST(" +(x< +y)<> not z",  +(x< +y)!= not z);
    CHECK_AST(" +x<( +y)<> not z",  +x<( +y)!= not z);
    CHECK_AST(" +x< +(y)<> not z",  +x< +(y)!= not z);
    CHECK_AST("( +x)< -y<>z", ( +x)< -y!=z);
    CHECK_AST("( +x< -y)<>z", ( +x< -y)!=z);
    CHECK_AST(" +(x)< -y<>z",  +(x)< -y!=z);
    CHECK_AST(" +(x< -y)<>z",  +(x< -y)!=z);
    CHECK_AST(" +x<( -y)<>z",  +x<( -y)!=z);
    CHECK_AST(" +x< -(y)<>z",  +x< -(y)!=z);
    CHECK_AST("( +x)< -y<> +z", ( +x)< -y!= +z);
    CHECK_AST("( +x< -y)<> +z", ( +x< -y)!= +z);
    CHECK_AST(" +(x)< -y<> +z",  +(x)< -y!= +z);
    CHECK_AST(" +(x< -y)<> +z",  +(x< -y)!= +z);
    CHECK_AST(" +x<( -y)<> +z",  +x<( -y)!= +z);
    CHECK_AST(" +x< -(y)<> +z",  +x< -(y)!= +z);
    CHECK_AST("( +x)< -y<> -z", ( +x)< -y!= -z);
    CHECK_AST("( +x< -y)<> -z", ( +x< -y)!= -z);
    CHECK_AST(" +(x)< -y<> -z",  +(x)< -y!= -z);
    CHECK_AST(" +(x< -y)<> -z",  +(x< -y)!= -z);
    CHECK_AST(" +x<( -y)<> -z",  +x<( -y)!= -z);
    CHECK_AST(" +x< -(y)<> -z",  +x< -(y)!= -z);
    CHECK_AST("( +x)< -y<> not z", ( +x)< -y!= not z);
    CHECK_AST("( +x< -y)<> not z", ( +x< -y)!= not z);
    CHECK_AST(" +(x)< -y<> not z",  +(x)< -y!= not z);
    CHECK_AST(" +(x< -y)<> not z",  +(x< -y)!= not z);
    CHECK_AST(" +x<( -y)<> not z",  +x<( -y)!= not z);
    CHECK_AST(" +x< -(y)<> not z",  +x< -(y)!= not z);
    CHECK_AST("( +x)< not y<>z", ( +x)< not y!=z);
    CHECK_AST("( +x< not y)<>z", ( +x< not y)!=z);
    CHECK_AST(" +(x)< not y<>z",  +(x)< not y!=z);
    CHECK_AST(" +(x< not y)<>z",  +(x< not y)!=z);
    CHECK_AST(" +x<( not y)<>z",  +x<( not y)!=z);
    CHECK_AST(" +x< not (y)<>z",  +x< not (y)!=z);
    CHECK_AST("( +x)< not y<> +z", ( +x)< not y!= +z);
    CHECK_AST("( +x< not y)<> +z", ( +x< not y)!= +z);
    CHECK_AST(" +(x)< not y<> +z",  +(x)< not y!= +z);
    CHECK_AST(" +(x< not y)<> +z",  +(x< not y)!= +z);
    CHECK_AST(" +x<( not y)<> +z",  +x<( not y)!= +z);
    CHECK_AST(" +x< not (y)<> +z",  +x< not (y)!= +z);
    CHECK_AST("( +x)< not y<> -z", ( +x)< not y!= -z);
    CHECK_AST("( +x< not y)<> -z", ( +x< not y)!= -z);
    CHECK_AST(" +(x)< not y<> -z",  +(x)< not y!= -z);
    CHECK_AST(" +(x< not y)<> -z",  +(x< not y)!= -z);
    CHECK_AST(" +x<( not y)<> -z",  +x<( not y)!= -z);
    CHECK_AST(" +x< not (y)<> -z",  +x< not (y)!= -z);
    CHECK_AST("( +x)< not y<> not z", ( +x)< not y!= not z);
    CHECK_AST("( +x< not y)<> not z", ( +x< not y)!= not z);
    CHECK_AST(" +(x)< not y<> not z",  +(x)< not y!= not z);
    CHECK_AST(" +(x< not y)<> not z",  +(x< not y)!= not z);
    CHECK_AST(" +x<( not y)<> not z",  +x<( not y)!= not z);
    CHECK_AST(" +x< not (y)<> not z",  +x< not (y)!= not z);
    CHECK_AST("( -x)<y<>z", ( -x)<y!=z);
    CHECK_AST("( -x<y)<>z", ( -x<y)!=z);
    CHECK_AST(" -(x)<y<>z",  -(x)<y!=z);
    CHECK_AST(" -(x<y)<>z",  -(x<y)!=z);
    CHECK_AST(" -x<(y)<>z",  -x<(y)!=z);
    CHECK_AST("( -x)<y<> +z", ( -x)<y!= +z);
    CHECK_AST("( -x<y)<> +z", ( -x<y)!= +z);
    CHECK_AST(" -(x)<y<> +z",  -(x)<y!= +z);
    CHECK_AST(" -(x<y)<> +z",  -(x<y)!= +z);
    CHECK_AST(" -x<(y)<> +z",  -x<(y)!= +z);
    CHECK_AST("( -x)<y<> -z", ( -x)<y!= -z);
    CHECK_AST("( -x<y)<> -z", ( -x<y)!= -z);
    CHECK_AST(" -(x)<y<> -z",  -(x)<y!= -z);
    CHECK_AST(" -(x<y)<> -z",  -(x<y)!= -z);
    CHECK_AST(" -x<(y)<> -z",  -x<(y)!= -z);
    CHECK_AST("( -x)<y<> not z", ( -x)<y!= not z);
    CHECK_AST("( -x<y)<> not z", ( -x<y)!= not z);
    CHECK_AST(" -(x)<y<> not z",  -(x)<y!= not z);
    CHECK_AST(" -(x<y)<> not z",  -(x<y)!= not z);
    CHECK_AST(" -x<(y)<> not z",  -x<(y)!= not z);
    CHECK_AST("( -x)< +y<>z", ( -x)< +y!=z);
    CHECK_AST("( -x< +y)<>z", ( -x< +y)!=z);
    CHECK_AST(" -(x)< +y<>z",  -(x)< +y!=z);
    CHECK_AST(" -(x< +y)<>z",  -(x< +y)!=z);
    CHECK_AST(" -x<( +y)<>z",  -x<( +y)!=z);
    CHECK_AST(" -x< +(y)<>z",  -x< +(y)!=z);
    CHECK_AST("( -x)< +y<> +z", ( -x)< +y!= +z);
    CHECK_AST("( -x< +y)<> +z", ( -x< +y)!= +z);
    CHECK_AST(" -(x)< +y<> +z",  -(x)< +y!= +z);
    CHECK_AST(" -(x< +y)<> +z",  -(x< +y)!= +z);
    CHECK_AST(" -x<( +y)<> +z",  -x<( +y)!= +z);
    CHECK_AST(" -x< +(y)<> +z",  -x< +(y)!= +z);
    CHECK_AST("( -x)< +y<> -z", ( -x)< +y!= -z);
    CHECK_AST("( -x< +y)<> -z", ( -x< +y)!= -z);
    CHECK_AST(" -(x)< +y<> -z",  -(x)< +y!= -z);
    CHECK_AST(" -(x< +y)<> -z",  -(x< +y)!= -z);
    CHECK_AST(" -x<( +y)<> -z",  -x<( +y)!= -z);
    CHECK_AST(" -x< +(y)<> -z",  -x< +(y)!= -z);
    CHECK_AST("( -x)< +y<> not z", ( -x)< +y!= not z);
    CHECK_AST("( -x< +y)<> not z", ( -x< +y)!= not z);
    CHECK_AST(" -(x)< +y<> not z",  -(x)< +y!= not z);
    CHECK_AST(" -(x< +y)<> not z",  -(x< +y)!= not z);
    CHECK_AST(" -x<( +y)<> not z",  -x<( +y)!= not z);
    CHECK_AST(" -x< +(y)<> not z",  -x< +(y)!= not z);
    CHECK_AST("( -x)< -y<>z", ( -x)< -y!=z);
    CHECK_AST("( -x< -y)<>z", ( -x< -y)!=z);
    CHECK_AST(" -(x)< -y<>z",  -(x)< -y!=z);
    CHECK_AST(" -(x< -y)<>z",  -(x< -y)!=z);
    CHECK_AST(" -x<( -y)<>z",  -x<( -y)!=z);
    CHECK_AST(" -x< -(y)<>z",  -x< -(y)!=z);
    CHECK_AST("( -x)< -y<> +z", ( -x)< -y!= +z);
    CHECK_AST("( -x< -y)<> +z", ( -x< -y)!= +z);
    CHECK_AST(" -(x)< -y<> +z",  -(x)< -y!= +z);
    CHECK_AST(" -(x< -y)<> +z",  -(x< -y)!= +z);
    CHECK_AST(" -x<( -y)<> +z",  -x<( -y)!= +z);
    CHECK_AST(" -x< -(y)<> +z",  -x< -(y)!= +z);
    CHECK_AST("( -x)< -y<> -z", ( -x)< -y!= -z);
    CHECK_AST("( -x< -y)<> -z", ( -x< -y)!= -z);
    CHECK_AST(" -(x)< -y<> -z",  -(x)< -y!= -z);
    CHECK_AST(" -(x< -y)<> -z",  -(x< -y)!= -z);
    CHECK_AST(" -x<( -y)<> -z",  -x<( -y)!= -z);
    CHECK_AST(" -x< -(y)<> -z",  -x< -(y)!= -z);
    CHECK_AST("( -x)< -y<> not z", ( -x)< -y!= not z);
    CHECK_AST("( -x< -y)<> not z", ( -x< -y)!= not z);
    CHECK_AST(" -(x)< -y<> not z",  -(x)< -y!= not z);
    CHECK_AST(" -(x< -y)<> not z",  -(x< -y)!= not z);
    CHECK_AST(" -x<( -y)<> not z",  -x<( -y)!= not z);
    CHECK_AST(" -x< -(y)<> not z",  -x< -(y)!= not z);
    CHECK_AST("( -x)< not y<>z", ( -x)< not y!=z);
    CHECK_AST("( -x< not y)<>z", ( -x< not y)!=z);
    CHECK_AST(" -(x)< not y<>z",  -(x)< not y!=z);
    CHECK_AST(" -(x< not y)<>z",  -(x< not y)!=z);
    CHECK_AST(" -x<( not y)<>z",  -x<( not y)!=z);
    CHECK_AST(" -x< not (y)<>z",  -x< not (y)!=z);
    CHECK_AST("( -x)< not y<> +z", ( -x)< not y!= +z);
    CHECK_AST("( -x< not y)<> +z", ( -x< not y)!= +z);
    CHECK_AST(" -(x)< not y<> +z",  -(x)< not y!= +z);
    CHECK_AST(" -(x< not y)<> +z",  -(x< not y)!= +z);
    CHECK_AST(" -x<( not y)<> +z",  -x<( not y)!= +z);
    CHECK_AST(" -x< not (y)<> +z",  -x< not (y)!= +z);
    CHECK_AST("( -x)< not y<> -z", ( -x)< not y!= -z);
    CHECK_AST("( -x< not y)<> -z", ( -x< not y)!= -z);
    CHECK_AST(" -(x)< not y<> -z",  -(x)< not y!= -z);
    CHECK_AST(" -(x< not y)<> -z",  -(x< not y)!= -z);
    CHECK_AST(" -x<( not y)<> -z",  -x<( not y)!= -z);
    CHECK_AST(" -x< not (y)<> -z",  -x< not (y)!= -z);
    CHECK_AST("( -x)< not y<> not z", ( -x)< not y!= not z);
    CHECK_AST("( -x< not y)<> not z", ( -x< not y)!= not z);
    CHECK_AST(" -(x)< not y<> not z",  -(x)< not y!= not z);
    CHECK_AST(" -(x< not y)<> not z",  -(x< not y)!= not z);
    CHECK_AST(" -x<( not y)<> not z",  -x<( not y)!= not z);
    CHECK_AST(" -x< not (y)<> not z",  -x< not (y)!= not z);
    CHECK_AST("( not x)<y<>z", ( not x)<y!=z);
    CHECK_AST("( not x<y)<>z", ( not x<y)!=z);
    CHECK_AST(" not (x)<y<>z",  not (x)<y!=z);
    CHECK_AST(" not (x<y)<>z",  not (x<y)!=z);
    CHECK_AST(" not x<(y)<>z",  not x<(y)!=z);
    CHECK_AST("( not x)<y<> +z", ( not x)<y!= +z);
    CHECK_AST("( not x<y)<> +z", ( not x<y)!= +z);
    CHECK_AST(" not (x)<y<> +z",  not (x)<y!= +z);
    CHECK_AST(" not (x<y)<> +z",  not (x<y)!= +z);
    CHECK_AST(" not x<(y)<> +z",  not x<(y)!= +z);
    CHECK_AST("( not x)<y<> -z", ( not x)<y!= -z);
    CHECK_AST("( not x<y)<> -z", ( not x<y)!= -z);
    CHECK_AST(" not (x)<y<> -z",  not (x)<y!= -z);
    CHECK_AST(" not (x<y)<> -z",  not (x<y)!= -z);
    CHECK_AST(" not x<(y)<> -z",  not x<(y)!= -z);
    CHECK_AST("( not x)<y<> not z", ( not x)<y!= not z);
    CHECK_AST("( not x<y)<> not z", ( not x<y)!= not z);
    CHECK_AST(" not (x)<y<> not z",  not (x)<y!= not z);
    CHECK_AST(" not (x<y)<> not z",  not (x<y)!= not z);
    CHECK_AST(" not x<(y)<> not z",  not x<(y)!= not z);
    CHECK_AST("( not x)< +y<>z", ( not x)< +y!=z);
    CHECK_AST("( not x< +y)<>z", ( not x< +y)!=z);
    CHECK_AST(" not (x)< +y<>z",  not (x)< +y!=z);
    CHECK_AST(" not (x< +y)<>z",  not (x< +y)!=z);
    CHECK_AST(" not x<( +y)<>z",  not x<( +y)!=z);
    CHECK_AST(" not x< +(y)<>z",  not x< +(y)!=z);
    CHECK_AST("( not x)< +y<> +z", ( not x)< +y!= +z);
    CHECK_AST("( not x< +y)<> +z", ( not x< +y)!= +z);
    CHECK_AST(" not (x)< +y<> +z",  not (x)< +y!= +z);
    CHECK_AST(" not (x< +y)<> +z",  not (x< +y)!= +z);
    CHECK_AST(" not x<( +y)<> +z",  not x<( +y)!= +z);
    CHECK_AST(" not x< +(y)<> +z",  not x< +(y)!= +z);
    CHECK_AST("( not x)< +y<> -z", ( not x)< +y!= -z);
    CHECK_AST("( not x< +y)<> -z", ( not x< +y)!= -z);
    CHECK_AST(" not (x)< +y<> -z",  not (x)< +y!= -z);
    CHECK_AST(" not (x< +y)<> -z",  not (x< +y)!= -z);
    CHECK_AST(" not x<( +y)<> -z",  not x<( +y)!= -z);
    CHECK_AST(" not x< +(y)<> -z",  not x< +(y)!= -z);
    CHECK_AST("( not x)< +y<> not z", ( not x)< +y!= not z);
    CHECK_AST("( not x< +y)<> not z", ( not x< +y)!= not z);
    CHECK_AST(" not (x)< +y<> not z",  not (x)< +y!= not z);
    CHECK_AST(" not (x< +y)<> not z",  not (x< +y)!= not z);
    CHECK_AST(" not x<( +y)<> not z",  not x<( +y)!= not z);
    CHECK_AST(" not x< +(y)<> not z",  not x< +(y)!= not z);
    CHECK_AST("( not x)< -y<>z", ( not x)< -y!=z);
    CHECK_AST("( not x< -y)<>z", ( not x< -y)!=z);
    CHECK_AST(" not (x)< -y<>z",  not (x)< -y!=z);
    CHECK_AST(" not (x< -y)<>z",  not (x< -y)!=z);
    CHECK_AST(" not x<( -y)<>z",  not x<( -y)!=z);
    CHECK_AST(" not x< -(y)<>z",  not x< -(y)!=z);
    CHECK_AST("( not x)< -y<> +z", ( not x)< -y!= +z);
    CHECK_AST("( not x< -y)<> +z", ( not x< -y)!= +z);
    CHECK_AST(" not (x)< -y<> +z",  not (x)< -y!= +z);
    CHECK_AST(" not (x< -y)<> +z",  not (x< -y)!= +z);
    CHECK_AST(" not x<( -y)<> +z",  not x<( -y)!= +z);
    CHECK_AST(" not x< -(y)<> +z",  not x< -(y)!= +z);
    CHECK_AST("( not x)< -y<> -z", ( not x)< -y!= -z);
    CHECK_AST("( not x< -y)<> -z", ( not x< -y)!= -z);
    CHECK_AST(" not (x)< -y<> -z",  not (x)< -y!= -z);
    CHECK_AST(" not (x< -y)<> -z",  not (x< -y)!= -z);
    CHECK_AST(" not x<( -y)<> -z",  not x<( -y)!= -z);
    CHECK_AST(" not x< -(y)<> -z",  not x< -(y)!= -z);
    CHECK_AST("( not x)< -y<> not z", ( not x)< -y!= not z);
    CHECK_AST("( not x< -y)<> not z", ( not x< -y)!= not z);
    CHECK_AST(" not (x)< -y<> not z",  not (x)< -y!= not z);
    CHECK_AST(" not (x< -y)<> not z",  not (x< -y)!= not z);
    CHECK_AST(" not x<( -y)<> not z",  not x<( -y)!= not z);
    CHECK_AST(" not x< -(y)<> not z",  not x< -(y)!= not z);
    CHECK_AST("( not x)< not y<>z", ( not x)< not y!=z);
    CHECK_AST("( not x< not y)<>z", ( not x< not y)!=z);
    CHECK_AST(" not (x)< not y<>z",  not (x)< not y!=z);
    CHECK_AST(" not (x< not y)<>z",  not (x< not y)!=z);
    CHECK_AST(" not x<( not y)<>z",  not x<( not y)!=z);
    CHECK_AST(" not x< not (y)<>z",  not x< not (y)!=z);
    CHECK_AST("( not x)< not y<> +z", ( not x)< not y!= +z);
    CHECK_AST("( not x< not y)<> +z", ( not x< not y)!= +z);
    CHECK_AST(" not (x)< not y<> +z",  not (x)< not y!= +z);
    CHECK_AST(" not (x< not y)<> +z",  not (x< not y)!= +z);
    CHECK_AST(" not x<( not y)<> +z",  not x<( not y)!= +z);
    CHECK_AST(" not x< not (y)<> +z",  not x< not (y)!= +z);
    CHECK_AST("( not x)< not y<> -z", ( not x)< not y!= -z);
    CHECK_AST("( not x< not y)<> -z", ( not x< not y)!= -z);
    CHECK_AST(" not (x)< not y<> -z",  not (x)< not y!= -z);
    CHECK_AST(" not (x< not y)<> -z",  not (x< not y)!= -z);
    CHECK_AST(" not x<( not y)<> -z",  not x<( not y)!= -z);
    CHECK_AST(" not x< not (y)<> -z",  not x< not (y)!= -z);
    CHECK_AST("( not x)< not y<> not z", ( not x)< not y!= not z);
    CHECK_AST("( not x< not y)<> not z", ( not x< not y)!= not z);
    CHECK_AST(" not (x)< not y<> not z",  not (x)< not y!= not z);
    CHECK_AST(" not (x< not y)<> not z",  not (x< not y)!= not z);
    CHECK_AST(" not x<( not y)<> not z",  not x<( not y)!= not z);
    CHECK_AST(" not x< not (y)<> not z",  not x< not (y)!= not z);
    CHECK_AST("(x)<y:=z", (x)<y=z);
    CHECK_AST("(x<y):=z", (x<y)=z);
    CHECK_AST("x<(y):=z", x<(y)=z);
    CHECK_AST("(x)<y:= +z", (x)<y= +z);
    CHECK_AST("(x<y):= +z", (x<y)= +z);
    CHECK_AST("x<(y):= +z", x<(y)= +z);
    CHECK_AST("(x)<y:= -z", (x)<y= -z);
    CHECK_AST("(x<y):= -z", (x<y)= -z);
    CHECK_AST("x<(y):= -z", x<(y)= -z);
    CHECK_AST("(x)<y:= not z", (x)<y= not z);
    CHECK_AST("(x<y):= not z", (x<y)= not z);
    CHECK_AST("x<(y):= not z", x<(y)= not z);
    CHECK_AST("(x)< +y:=z", (x)< +y=z);
    CHECK_AST("(x< +y):=z", (x< +y)=z);
    CHECK_AST("x<( +y):=z", x<( +y)=z);
    CHECK_AST("x< +(y):=z", x< +(y)=z);
    CHECK_AST("(x)< +y:= +z", (x)< +y= +z);
    CHECK_AST("(x< +y):= +z", (x< +y)= +z);
    CHECK_AST("x<( +y):= +z", x<( +y)= +z);
    CHECK_AST("x< +(y):= +z", x< +(y)= +z);
    CHECK_AST("(x)< +y:= -z", (x)< +y= -z);
    CHECK_AST("(x< +y):= -z", (x< +y)= -z);
    CHECK_AST("x<( +y):= -z", x<( +y)= -z);
    CHECK_AST("x< +(y):= -z", x< +(y)= -z);
    CHECK_AST("(x)< +y:= not z", (x)< +y= not z);
    CHECK_AST("(x< +y):= not z", (x< +y)= not z);
    CHECK_AST("x<( +y):= not z", x<( +y)= not z);
    CHECK_AST("x< +(y):= not z", x< +(y)= not z);
    CHECK_AST("(x)< -y:=z", (x)< -y=z);
    CHECK_AST("(x< -y):=z", (x< -y)=z);
    CHECK_AST("x<( -y):=z", x<( -y)=z);
    CHECK_AST("x< -(y):=z", x< -(y)=z);
    CHECK_AST("(x)< -y:= +z", (x)< -y= +z);
    CHECK_AST("(x< -y):= +z", (x< -y)= +z);
    CHECK_AST("x<( -y):= +z", x<( -y)= +z);
    CHECK_AST("x< -(y):= +z", x< -(y)= +z);
    CHECK_AST("(x)< -y:= -z", (x)< -y= -z);
    CHECK_AST("(x< -y):= -z", (x< -y)= -z);
    CHECK_AST("x<( -y):= -z", x<( -y)= -z);
    CHECK_AST("x< -(y):= -z", x< -(y)= -z);
    CHECK_AST("(x)< -y:= not z", (x)< -y= not z);
    CHECK_AST("(x< -y):= not z", (x< -y)= not z);
    CHECK_AST("x<( -y):= not z", x<( -y)= not z);
    CHECK_AST("x< -(y):= not z", x< -(y)= not z);
    CHECK_AST("(x)< not y:=z", (x)< not y=z);
    CHECK_AST("(x< not y):=z", (x< not y)=z);
    CHECK_AST("x<( not y):=z", x<( not y)=z);
    CHECK_AST("x< not (y):=z", x< not (y)=z);
    CHECK_AST("(x)< not y:= +z", (x)< not y= +z);
    CHECK_AST("(x< not y):= +z", (x< not y)= +z);
    CHECK_AST("x<( not y):= +z", x<( not y)= +z);
    CHECK_AST("x< not (y):= +z", x< not (y)= +z);
    CHECK_AST("(x)< not y:= -z", (x)< not y= -z);
    CHECK_AST("(x< not y):= -z", (x< not y)= -z);
    CHECK_AST("x<( not y):= -z", x<( not y)= -z);
    CHECK_AST("x< not (y):= -z", x< not (y)= -z);
    CHECK_AST("(x)< not y:= not z", (x)< not y= not z);
    CHECK_AST("(x< not y):= not z", (x< not y)= not z);
    CHECK_AST("x<( not y):= not z", x<( not y)= not z);
    CHECK_AST("x< not (y):= not z", x< not (y)= not z);
    CHECK_AST("( +x)<y:=z", ( +x)<y=z);
    CHECK_AST("( +x<y):=z", ( +x<y)=z);
    CHECK_AST(" +(x)<y:=z",  +(x)<y=z);
    CHECK_AST(" +(x<y):=z",  +(x<y)=z);
    CHECK_AST(" +x<(y):=z",  +x<(y)=z);
    CHECK_AST("( +x)<y:= +z", ( +x)<y= +z);
    CHECK_AST("( +x<y):= +z", ( +x<y)= +z);
    CHECK_AST(" +(x)<y:= +z",  +(x)<y= +z);
    CHECK_AST(" +(x<y):= +z",  +(x<y)= +z);
    CHECK_AST(" +x<(y):= +z",  +x<(y)= +z);
    CHECK_AST("( +x)<y:= -z", ( +x)<y= -z);
    CHECK_AST("( +x<y):= -z", ( +x<y)= -z);
    CHECK_AST(" +(x)<y:= -z",  +(x)<y= -z);
    CHECK_AST(" +(x<y):= -z",  +(x<y)= -z);
    CHECK_AST(" +x<(y):= -z",  +x<(y)= -z);
    CHECK_AST("( +x)<y:= not z", ( +x)<y= not z);
    CHECK_AST("( +x<y):= not z", ( +x<y)= not z);
    CHECK_AST(" +(x)<y:= not z",  +(x)<y= not z);
    CHECK_AST(" +(x<y):= not z",  +(x<y)= not z);
    CHECK_AST(" +x<(y):= not z",  +x<(y)= not z);
    CHECK_AST("( +x)< +y:=z", ( +x)< +y=z);
    CHECK_AST("( +x< +y):=z", ( +x< +y)=z);
    CHECK_AST(" +(x)< +y:=z",  +(x)< +y=z);
    CHECK_AST(" +(x< +y):=z",  +(x< +y)=z);
    CHECK_AST(" +x<( +y):=z",  +x<( +y)=z);
    CHECK_AST(" +x< +(y):=z",  +x< +(y)=z);
    CHECK_AST("( +x)< +y:= +z", ( +x)< +y= +z);
    CHECK_AST("( +x< +y):= +z", ( +x< +y)= +z);
    CHECK_AST(" +(x)< +y:= +z",  +(x)< +y= +z);
    CHECK_AST(" +(x< +y):= +z",  +(x< +y)= +z);
    CHECK_AST(" +x<( +y):= +z",  +x<( +y)= +z);
    CHECK_AST(" +x< +(y):= +z",  +x< +(y)= +z);
    CHECK_AST("( +x)< +y:= -z", ( +x)< +y= -z);
    CHECK_AST("( +x< +y):= -z", ( +x< +y)= -z);
    CHECK_AST(" +(x)< +y:= -z",  +(x)< +y= -z);
    CHECK_AST(" +(x< +y):= -z",  +(x< +y)= -z);
    CHECK_AST(" +x<( +y):= -z",  +x<( +y)= -z);
    CHECK_AST(" +x< +(y):= -z",  +x< +(y)= -z);
    CHECK_AST("( +x)< +y:= not z", ( +x)< +y= not z);
    CHECK_AST("( +x< +y):= not z", ( +x< +y)= not z);
    CHECK_AST(" +(x)< +y:= not z",  +(x)< +y= not z);
    CHECK_AST(" +(x< +y):= not z",  +(x< +y)= not z);
    CHECK_AST(" +x<( +y):= not z",  +x<( +y)= not z);
    CHECK_AST(" +x< +(y):= not z",  +x< +(y)= not z);

    auto total = good + bad;
    std::cout
        << "check_ast_bc: " << good << " out of " << total
        << " (" << std::setprecision(1) << std::fixed << (100.0*good/total) << "%)\n";
}