check_ast_bh.cpp

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

void check_ast_bh(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>= 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);
    CHECK_AST("( +x)<= -y<>z", ( +x)<= -y!=z);
    CHECK_AST("( +x<= -y)<>z", ( +x<= -y)!=z);
    CHECK_AST(" +(x)<= -y<>z",  +(x)<= -y!=z);
    CHECK_AST(" +(x<= -y)<>z",  +(x<= -y)!=z);
    CHECK_AST(" +x<=( -y)<>z",  +x<=( -y)!=z);
    CHECK_AST(" +x<= -(y)<>z",  +x<= -(y)!=z);
    CHECK_AST("( +x)<= -y<> +z", ( +x)<= -y!= +z);
    CHECK_AST("( +x<= -y)<> +z", ( +x<= -y)!= +z);
    CHECK_AST(" +(x)<= -y<> +z",  +(x)<= -y!= +z);
    CHECK_AST(" +(x<= -y)<> +z",  +(x<= -y)!= +z);
    CHECK_AST(" +x<=( -y)<> +z",  +x<=( -y)!= +z);
    CHECK_AST(" +x<= -(y)<> +z",  +x<= -(y)!= +z);
    CHECK_AST("( +x)<= -y<> -z", ( +x)<= -y!= -z);
    CHECK_AST("( +x<= -y)<> -z", ( +x<= -y)!= -z);
    CHECK_AST(" +(x)<= -y<> -z",  +(x)<= -y!= -z);
    CHECK_AST(" +(x<= -y)<> -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);

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