check_ast_ce.cpp

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

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

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