rewrite

decompiled_code:
__int64 __fastcall rewrite(__int64 a1, unsigned int a2, _QWORD *a3)
{
int v5; // eax
__int64 *v6; // rbx
__int64 v7; // rdi
_QWORD *v8; // rax
__int64 v9; // rbx
__int64 v10; // rdi
__int64 result; // rax
bool v12; // zf
_QWORD *v13; // rax
_QWORD *v14; // rax
__int64 v15; // rbx
__int64 v16; // rdi
__int64 v17; // rbx
_QWORD *v18; // r14
__int64 v19; // r12
__int64 v20; // rbx
__int64 v21; // rdi

while ( 2 )
{
if ( (unsigned int)term_flag(a1, a2) || *(int *)a1 >= 0 )
return a1;
v5 = -*(_DWORD *)a1;
if ( v5 >= Symbols_size )
goto LABEL_13;
v6 = *(__int64 **)(a1 + 8);
v7 = *v6;
switch ( *(_DWORD *)(Op_codes + 4LL * v5) )
{
case 0x11:
case 0x13:
*v6 = rewrite(v7, a2, a3);
if ( (unsigned int)true_term(**(_QWORD **)(a1 + 8)) )
goto LABEL_6;
if ( !(unsigned int)false_term(**(_QWORD **)(a1 + 8)) )
goto LABEL_13;
zap_term(a1);
return bool_to_term(0LL);
case 0x12:
case 0x14:
*v6 = rewrite(v7, a2, a3);
if ( (unsigned int)false_term(**(_QWORD **)(a1 + 8)) )
{
LABEL_6:
v8 = *(_QWORD **)(a1 + 8);
v9 = v8[1];
zap_term(*v8);
v10 = a1;
a1 = v9;
free_term(v10);
continue;
}
if ( (unsigned int)true_term(**(_QWORD **)(a1 + 8)) )
{
zap_term(a1);
result = bool_to_term(1LL);
}
else
{
LABEL_13:
v17 = 0LL;
if ( *(_BYTE *)(a1 + 4) )
{
do
{
v18 = (_QWORD *)(*(_QWORD *)(a1 + 8) + 8 * v17++);
*v18 = rewrite(*v18, a2, a3);
}
while ( *(unsigned __int8 *)(a1 + 4) > (int)v17 );
}
v19 = rewrite_top((_DWORD *)a1, a2, a3);
term_flag_set(v19, a2);
result = v19;
}
return result;
case 0x15:
*v6 = rewrite(v7, a2, a3);
v12 = (unsigned int)true_term(**(_QWORD **)(a1 + 8)) == 0;
v13 = *(_QWORD **)(a1 + 8);
if ( v12 )
{
if ( !(unsigned int)false_term(*v13) )
goto LABEL_13;
v14 = *(_QWORD **)(a1 + 8);
v15 = v14[2];
zap_term(*v14);
zap_term(*(_QWORD *)(*(_QWORD *)(a1 + 8) + 8LL));
v16 = a1;
a1 = v15;
free_term(v16);
}
else
{
v20 = v13[1];
zap_term(*v13);
zap_term(*(_QWORD *)(*(_QWORD *)(a1 + 8) + 16LL));
v21 = a1;
a1 = v20;
free_term(v21);
}
continue;
default:
goto LABEL_13;
}
}
}

canonical_decompiled_code:
__int64 __fastcall func3(__int64 a1, unsigned int a2, _QWORD *a3)
{
int v5; // eax
__int64 *v6; // rbx
__int64 v7; // rdi
_QWORD *v8; // rax
__int64 v9; // rbx
__int64 v10; // rdi
__int64 result; // rax
bool v12; // zf
_QWORD *v13; // rax
_QWORD *v14; // rax
__int64 v15; // rbx
__int64 v16; // rdi
__int64 v17; // rbx
_QWORD *v18; // r14
__int64 v19; // r12
__int64 v20; // rbx
__int64 v21; // rdi

while ( 2 )
{
if ( (unsigned int)term_flag(a1, a2) || *(int *)a1 >= 0 )
return a1;
v5 = -*(_DWORD *)a1;
if ( v5 >= Symbols_size )
goto LABEL_13;
v6 = *(__int64 **)(a1 + 8);
v7 = *v6;
switch ( *(_DWORD *)(Op_codes + 4LL * v5) )
{
case 0x11:
case 0x13:
*v6 = func3(v7, a2, a3);
if ( (unsigned int)true_term(**(_QWORD **)(a1 + 8)) )
goto LABEL_6;
if ( !(unsigned int)false_term(**(_QWORD **)(a1 + 8)) )
goto LABEL_13;
zap_term(a1);
return bool_to_term(0LL);
case 0x12:
case 0x14:
*v6 = func3(v7, a2, a3);
if ( (unsigned int)false_term(**(_QWORD **)(a1 + 8)) )
{
LABEL_6:
v8 = *(_QWORD **)(a1 + 8);
v9 = v8[1];
zap_term(*v8);
v10 = a1;
a1 = v9;
free_term(v10);
continue;
}
if ( (unsigned int)true_term(**(_QWORD **)(a1 + 8)) )
{
zap_term(a1);
result = bool_to_term(1LL);
}
else
{
LABEL_13:
v17 = 0LL;
if ( *(_BYTE *)(a1 + 4) )
{
do
{
v18 = (_QWORD *)(*(_QWORD *)(a1 + 8) + 8 * v17++);
*v18 = func3(*v18, a2, a3);
}
while ( *(unsigned __int8 *)(a1 + 4) > (int)v17 );
}
v19 = func2((_DWORD *)a1, a2, a3);
term_flag_set(v19, a2);
result = v19;
}
return result;
case 0x15:
*v6 = func3(v7, a2, a3);
v12 = (unsigned int)true_term(**(_QWORD **)(a1 + 8)) == 0;
v13 = *(_QWORD **)(a1 + 8);
if ( v12 )
{
if ( !(unsigned int)false_term(*v13) )
goto LABEL_13;
v14 = *(_QWORD **)(a1 + 8);
v15 = v14[2];
zap_term(*v14);
zap_term(*(_QWORD *)(*(_QWORD *)(a1 + 8) + 8LL));
v16 = a1;
a1 = v15;
free_term(v16);
}
else
{
v20 = v13[1];
zap_term(*v13);
zap_term(*(_QWORD *)(*(_QWORD *)(a1 + 8) + 16LL));
v21 = a1;
a1 = v20;
free_term(v21);
}
continue;
default:
goto LABEL_13;
}
}
}

original_code:
static
Term rewrite(Term t, int flag, I3list *steps)
{
  if (term_flag(t, flag) || ((t)->private_symbol >= 0))
    return t;
  else {
    int op_code = ((-((t)->private_symbol)) < Symbols_size ? Op_codes[(-((t)->private_symbol))] : -1);
    int i;
    switch (op_code) {
    case AND_OP:
    case AND2_OP:
      ((t)->args[0]) = rewrite(((t)->args[0]), flag, steps);
      if (true_term(((t)->args[0]))) {
 Term tmp = ((t)->args[1]);
 zap_term(((t)->args[0]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      else if (false_term(((t)->args[0]))) {
 zap_term(t);
 return bool_to_term(FALSE);
      }
      break;
    case OR_OP:
    case OR2_OP:
      ((t)->args[0]) = rewrite(((t)->args[0]), flag, steps);
      if (false_term(((t)->args[0]))) {
 Term tmp = ((t)->args[1]);
 zap_term(((t)->args[0]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      else if (true_term(((t)->args[0]))) {
 zap_term(t);
 return bool_to_term(TRUE);
      }
      break;
    case IF_OP:
      ((t)->args[0]) = rewrite(((t)->args[0]), flag, steps);
      if (true_term(((t)->args[0]))) {
 Term tmp = ((t)->args[1]);
 zap_term(((t)->args[0]));
 zap_term(((t)->args[2]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      else if (false_term(((t)->args[0]))) {
 Term tmp = ((t)->args[2]);
 zap_term(((t)->args[0]));
 zap_term(((t)->args[1]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      break;
    }
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = rewrite(((t)->args[i]), flag, steps);
    t = rewrite_top(t, flag, steps);
    term_flag_set(t, flag);
    return t;
  }
}

canonical_original_code:
static struct term *rewrite(struct term *t, int flag, struct i3list **steps)
{
  if (term_flag(t, flag) || ((t)->private_symbol >= 0))
    return t;
  else {
    int op_code = ((-((t)->private_symbol)) < Symbols_size ? Op_codes[(-((t)->private_symbol))] : -1);
    int i;
    switch (op_code) {
    case AND_OP:
    case AND2_OP:
      ((t)->args[0]) = rewrite(((t)->args[0]), flag, steps);
      if (true_term(((t)->args[0]))) {
 struct term *tmp = ((t)->args[1]);
 zap_term(((t)->args[0]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      else if (false_term(((t)->args[0]))) {
 zap_term(t);
 return bool_to_term(FALSE);
      }
      break;
    case OR_OP:
    case OR2_OP:
      ((t)->args[0]) = rewrite(((t)->args[0]), flag, steps);
      if (false_term(((t)->args[0]))) {
 struct term *tmp = ((t)->args[1]);
 zap_term(((t)->args[0]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      else if (true_term(((t)->args[0]))) {
 zap_term(t);
 return bool_to_term(TRUE);
      }
      break;
    case IF_OP:
      ((t)->args[0]) = rewrite(((t)->args[0]), flag, steps);
      if (true_term(((t)->args[0]))) {
 struct term *tmp = ((t)->args[1]);
 zap_term(((t)->args[0]));
 zap_term(((t)->args[2]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      else if (false_term(((t)->args[0]))) {
 struct term *tmp = ((t)->args[2]);
 zap_term(((t)->args[0]));
 zap_term(((t)->args[1]));
 free_term(t);
 return rewrite(tmp, flag, steps);
      }
      break;
    }
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = rewrite(((t)->args[i]), flag, steps);
    t = rewrite_top(t, flag, steps);
    term_flag_set(t, flag);
    return t;
  }
}

variable_types: flag int

variable_types: struct i3list { int i; int j; int k; struct i3list *next; } **


repo: jessealama/ladr

decompiled_code:
void __fastcall mace4_sig_handler(unsigned int a1)
{
printf("\nmace4_sig_handler: condition %d", a1);
switch ( a1 )
{
case 0xAu:
p_stats();
fflush(stdout);
break;
case 0xBu:
p_stats();
mace4_exit(102LL);
break;
case 2u:
p_stats();
mace4_exit(101LL);
break;
default:
fatal_error("mace4_sig_handler, unknown signal");
break;
}
}

canonical_decompiled_code:
void __fastcall func0(unsigned int a1)
{
printf("\nmace4_sig_handler: condition %d", a1);
switch ( a1 )
{
case 0xAu:
p_stats();
fflush(stdout);
break;
case 0xBu:
p_stats();
mace4_exit(102LL);
break;
case 2u:
p_stats();
mace4_exit(101LL);
break;
default:
fatal_error("mace4_sig_handler, unknown signal");
break;
}
}

original_code:
void mace4_sig_handler(int condition)
{
  printf("\nmace4_sig_handler: condition %d", condition);
  switch (condition) {
  case 11:
    p_stats();
    mace4_exit(MACE_SIGSEGV_EXIT);
    break;
  case 2:
    p_stats();
    mace4_exit(MACE_SIGINT_EXIT);
    break;
  case 10:
    p_stats();
    fflush(stdout);
    break;
  default: fatal_error("mace4_sig_handler, unknown signal");
  }
}

variable_types: condition int

return_type: void


decompiled_code:
__int64 init_attrs()
{
register_attribute("label", 1LL);
register_attribute("bsub_hint_wt", 0LL);
register_attribute("answer", 2LL);
register_attribute("action", 2LL);
return register_attribute("action2", 2LL);
}

canonical_decompiled_code:
__int64 func1()
{
register_attribute("label", 1LL);
register_attribute("bsub_hint_wt", 0LL);
register_attribute("answer", 2LL);
register_attribute("action", 2LL);
return register_attribute("action2", 2LL);
}

original_code:
void init_attrs(void)
{
  int id;
  id = register_attribute("label", STRING_ATTRIBUTE);
  id = register_attribute("bsub_hint_wt", INT_ATTRIBUTE);
  id = register_attribute("answer", TERM_ATTRIBUTE);
  id = register_attribute("action", TERM_ATTRIBUTE);
  id = register_attribute("action2", TERM_ATTRIBUTE);
}

canonical_original_code:
void init_attrs()
{
  int id;
  id = register_attribute("label", STRING_ATTRIBUTE);
  id = register_attribute("bsub_hint_wt", INT_ATTRIBUTE);
  id = register_attribute("answer", TERM_ATTRIBUTE);
  id = register_attribute("action", TERM_ATTRIBUTE);
  id = register_attribute("action2", TERM_ATTRIBUTE);
}

variable_types: id int


decompiled_code:
__int64 __fastcall read_mace4_input(unsigned int a1, __int64 a2, int a3, __int64 a4)
{
__int64 v6; // rax
__int64 v8; // [rsp+8h] [rbp-50h] BYREF
__int64 v9; // [rsp+10h] [rbp-48h] BYREF
_QWORD *v10; // [rsp+18h] [rbp-40h] BYREF
__int64 v11; // [rsp+20h] [rbp-38h] BYREF
__int64 v12[6]; // [rsp+28h] [rbp-30h] BYREF

accept_list("hints", 1LL, 1LL, v12);
accept_list("goals", 1LL, 0LL, &v9);
accept_list("distinct", 0LL, 0LL, &v10);
accept_list(&unk_53A, 1LL, 0LL, &v8);
accept_list(&unk_53A, 0LL, 0LL, &v11);
print_separator(stdout, "INPUT", 1LL);
read_all_input(a1, a2, stdout, 1LL, (unsigned int)(a3 == 0) + 2);
if ( v11 )
printf("%% term list(s) ignored\n");
if ( v12[0] )
printf("%% hints list(s) ignored\n");
process_command_line_args(a1, a2, a4);
print_separator(stdout, "end of input", 1LL);
if ( !(unsigned int)option_dependencies_state() )
{
printf("\n%% Enabling option dependencies (ignore applies only on input).\n");
enable_option_dependencies();
}
v6 = process_distinct_terms(v10);
v8 = plist_cat(v8, v6);
v8 = embed_formulas_in_topforms(v8, 1LL);
v9 = embed_formulas_in_topforms(v9, 0LL);
print_separator(stdout, "PROCESS NON-CLAUSAL FORMULAS", 1LL);
printf("\n%% Formulas that are not ordinary clauses:\n");
v8 = process_input_formulas(v8, 1LL);
v9 = process_goal_formulas(v9, 1LL);
print_separator(stdout, "end of process non-clausal formulas", 1LL);
return plist_cat(v8, v9);
}

canonical_decompiled_code:
__int64 __fastcall func3(unsigned int a1, __int64 a2, int a3, __int64 a4)
{
__int64 v6; // rax
__int64 v8; // [rsp+8h] [rbp-50h] BYREF
__int64 v9; // [rsp+10h] [rbp-48h] BYREF
_QWORD *v10; // [rsp+18h] [rbp-40h] BYREF
__int64 v11; // [rsp+20h] [rbp-38h] BYREF
__int64 v12[6]; // [rsp+28h] [rbp-30h] BYREF

accept_list("hints", 1LL, 1LL, v12);
accept_list("goals", 1LL, 0LL, &v9);
accept_list("distinct", 0LL, 0LL, &v10);
accept_list(&unk_53A, 1LL, 0LL, &v8);
accept_list(&unk_53A, 0LL, 0LL, &v11);
print_separator(stdout, "INPUT", 1LL);
read_all_input(a1, a2, stdout, 1LL, (unsigned int)(a3 == 0) + 2);
if ( v11 )
printf("%% term list(s) ignored\n");
if ( v12[0] )
printf("%% hints list(s) ignored\n");
process_command_line_args(a1, a2, a4);
print_separator(stdout, "end of input", 1LL);
if ( !(unsigned int)option_dependencies_state() )
{
printf("\n%% Enabling option dependencies (ignore applies only on input).\n");
enable_option_dependencies();
}
v6 = func2(v10);
v8 = plist_cat(v8, v6);
v8 = embed_formulas_in_topforms(v8, 1LL);
v9 = embed_formulas_in_topforms(v9, 0LL);
print_separator(stdout, "PROCESS NON-CLAUSAL FORMULAS", 1LL);
printf("\n%% Formulas that are not ordinary clauses:\n");
v8 = process_input_formulas(v8, 1LL);
v9 = process_goal_formulas(v9, 1LL);
print_separator(stdout, "end of process non-clausal formulas", 1LL);
return plist_cat(v8, v9);
}

original_code:
static
Plist read_mace4_input(int argc, char **argv, BOOL allow_unknown_things,
        Mace_options opt)
{
  Plist wild_formulas, goals;
  Plist distinct_lists, distinct_forms;
  Plist wild_terms, hints;
  accept_list("hints", FORMULAS, TRUE, &hints);
  accept_list("goals", FORMULAS, FALSE, &goals);
  accept_list("distinct", TERMS, FALSE, &distinct_lists);
  accept_list("", FORMULAS, FALSE, &wild_formulas);
  accept_list("", TERMS, FALSE, &wild_terms);
  print_separator(stdout, "INPUT", TRUE);
  read_all_input(argc, argv, stdout, TRUE,
   allow_unknown_things ? WARN_UNKNOWN : KILL_UNKNOWN);
  if (wild_terms)
    printf("%%   term list(s) ignored\n");
  if (hints)
    printf("%%   hints list(s) ignored\n");
  process_command_line_args(argc, argv, opt);
  print_separator(stdout, "end of input", TRUE);
  if (!option_dependencies_state()) {
    printf("\n%% Enabling option dependencies (ignore applies only on input).\n");
    enable_option_dependencies();
  }
  distinct_forms = process_distinct_terms(distinct_lists);
  wild_formulas = plist_cat(wild_formulas, distinct_forms);
  wild_formulas = embed_formulas_in_topforms(wild_formulas, TRUE);
  goals = embed_formulas_in_topforms(goals, FALSE);
  print_separator(stdout, "PROCESS NON-CLAUSAL FORMULAS", TRUE);
  printf("\n%% Formulas that are not ordinary clauses:\n");
  wild_formulas = process_input_formulas(wild_formulas, TRUE);
  goals = process_goal_formulas(goals, TRUE);
  print_separator(stdout, "end of process non-clausal formulas", TRUE);
  wild_formulas = plist_cat(wild_formulas, goals);
  return wild_formulas;
}

canonical_original_code:
static struct plist *read_mace4_input(int argc, char **argv, enum BOOL allow_unknown_things, struct mace_options *opt)
{
  struct plist *wild_formulas; struct plist *goals;
  struct plist *distinct_lists; struct plist *distinct_forms;
  struct plist *wild_terms; struct plist *hints;
  accept_list("hints", FORMULAS, TRUE, &hints);
  accept_list("goals", FORMULAS, FALSE, &goals);
  accept_list("distinct", TERMS, FALSE, &distinct_lists);
  accept_list("", FORMULAS, FALSE, &wild_formulas);
  accept_list("", TERMS, FALSE, &wild_terms);
  print_separator(stdout, "INPUT", TRUE);
  read_all_input(argc, argv, stdout, TRUE,
   allow_unknown_things ? WARN_UNKNOWN : KILL_UNKNOWN);
  if (wild_terms)
    printf("%%   term list(s) ignored\n");
  if (hints)
    printf("%%   hints list(s) ignored\n");
  process_command_line_args(argc, argv, opt);
  print_separator(stdout, "end of input", TRUE);
  if (!option_dependencies_state()) {
    printf("\n%% Enabling option dependencies (ignore applies only on input).\n");
    enable_option_dependencies();
  }
  distinct_forms = process_distinct_terms(distinct_lists);
  wild_formulas = plist_cat(wild_formulas, distinct_forms);
  wild_formulas = embed_formulas_in_topforms(wild_formulas, TRUE);
  goals = embed_formulas_in_topforms(goals, FALSE);
  print_separator(stdout, "PROCESS NON-CLAUSAL FORMULAS", TRUE);
  printf("\n%% Formulas that are not ordinary clauses:\n");
  wild_formulas = process_input_formulas(wild_formulas, TRUE);
  goals = process_goal_formulas(goals, TRUE);
  print_separator(stdout, "end of process non-clausal formulas", TRUE);
  wild_formulas = plist_cat(wild_formulas, goals);
  return wild_formulas;
}

variable_types: argc int

variable_types:
argv
char **

variable_types: struct mace_options { int print_models; int domain_size; int iterate; } *

variable_types: struct plist { void *v; struct plist *next; } *


main

canonical_name: main

decompiled_code:
int __cdecl __noreturn main(int argc, const char **argv, const char **envp)
{
int v3; // er13
__int64 v4; // rbp
__int64 v5; // rax
_BYTE v6[152]; // [rsp+0h] [rbp-98h] BYREF

v3 = member_args(argc, argv, "-c");
init_standard_ladr();
init_mace_options(v6);
init_attrs();
if ( !(unsigned int)member_args((unsigned int)argc, argv, "help")
&& !(unsigned int)member_args((unsigned int)argc, argv, "-help") )
{
print_banner((unsigned int)argc, argv, "Mace4", "2009-11A", "November 2009", 0LL);
set_program_name("Mace4");
signal(2, (__sighandler_t)mace4_sig_handler);
signal(10, (__sighandler_t)mace4_sig_handler);
signal(11, (__sighandler_t)mace4_sig_handler);
v4 = read_mace4_input(argc, (__int64)argv, v3, (__int64)v6);
print_separator(stdout, "CLAUSES FOR SEARCH", 1LL);
fwrite_clause_list(stdout, v4, "mace4_clauses", 1LL);
print_separator(stdout, "end of clauses for search", 1LL);
v5 = mace4(v4, v6);
mace4_exit(*(unsigned int *)(v5 + 24));
exit(0);
}
usage_message(stderr, v6);
exit(1);
}

canonical_decompiled_code:
int __cdecl __noreturn main(int argc, const char **argv, const char **envp)
{
int v3; // er13
__int64 v4; // rbp
__int64 v5; // rax
_BYTE v6[152]; // [rsp+0h] [rbp-98h] BYREF

v3 = member_args(argc, argv, "-c");
init_standard_ladr();
init_mace_options(v6);
func1();
if ( !(unsigned int)member_args((unsigned int)argc, argv, "help")
&& !(unsigned int)member_args((unsigned int)argc, argv, "-help") )
{
print_banner((unsigned int)argc, argv, "Mace4", "2009-11A", "November 2009", 0LL);
set_program_name("Mace4");
signal(2, (__sighandler_t)mace4_sig_handler);
signal(10, (__sighandler_t)mace4_sig_handler);
signal(11, (__sighandler_t)mace4_sig_handler);
v4 = func3(argc, (__int64)argv, v3, (__int64)v6);
print_separator(stdout, "CLAUSES FOR SEARCH", 1LL);
fwrite_clause_list(stdout, v4, "mace4_clauses", 1LL);
print_separator(stdout, "end of clauses for search", 1LL);
v5 = mace4(v4, v6);
mace4_exit(*(unsigned int *)(v5 + 24));
exit(0);
}
usage_message(stderr, v6);
exit(1);
}

original_code:
int main(int argc, char **argv)
{
  struct mace_options opt;
  Plist clauses;
  Mace_results results;
  BOOL prover_compatability_mode = member_args(argc, argv, "-c");
  init_standard_ladr();
  init_mace_options(&opt);
  init_attrs();
  if (member_args(argc, argv, "help") ||
      member_args(argc, argv, "-help")) {
    usage_message(stderr, &opt);
    exit(1);
  }
  print_banner(argc, argv, "Mace4", "2009-11A", "November 2009", FALSE);
  set_program_name("Mace4");
  signal(2, mace4_sig_handler);
  signal(10, mace4_sig_handler);
  signal(11, mace4_sig_handler);
  clauses = read_mace4_input(argc, argv, prover_compatability_mode, &opt);
  print_separator(stdout, "CLAUSES FOR SEARCH", TRUE);
  fwrite_clause_list(stdout, clauses, "mace4_clauses", CL_FORM_BARE);
  print_separator(stdout, "end of clauses for search", TRUE);
  results = mace4(clauses, &opt);
  mace4_exit(results->return_code);
  exit(0);
}

canonical_original_code:
int main(int argc, char **argv)
{
  struct mace_options opt;
  struct plist *clauses;
  struct mace_results *results;
  enum BOOL prover_compatability_mode = member_args(argc, argv, "-c");
  init_standard_ladr();
  init_mace_options(&opt);
  init_attrs();
  if (member_args(argc, argv, "help") ||
      member_args(argc, argv, "-help")) {
    usage_message(stderr, &opt);
    exit(1);
  }
  print_banner(argc, argv, "Mace4", "2009-11A", "November 2009", FALSE);
  set_program_name("Mace4");
  signal(2, mace4_sig_handler);
  signal(10, mace4_sig_handler);
  signal(11, mace4_sig_handler);
  clauses = read_mace4_input(argc, argv, prover_compatability_mode, &opt);
  print_separator(stdout, "CLAUSES FOR SEARCH", TRUE);
  fwrite_clause_list(stdout, clauses, "mace4_clauses", CL_FORM_BARE);
  print_separator(stdout, "end of clauses for search", TRUE);
  results = mace4(clauses, &opt);
  mace4_exit(results->return_code);
  exit(0);
}

variable_types: struct mace_options { int print_models; int domain_size; int iterate; }

variable_types: struct mace_results { enum BOOL { FALSE=0, TRUE=1 } success; struct plist { void *v; struct plist *next; } *models; double user_seconds; int return_code; } *

return_type: int

user_defined_types: struct mace_results { enum BOOL success; struct plist *models; double user_seconds; int return_code; }


decompiled_code:
__int64 __fastcall pvalues_check(__int64 *a1, int a2)
{
__int64 v2; // r8
__int64 v3; // rdx
__int64 result; // rax

if ( a2 <= 0 )
{
LABEL_10:
fatal_error("pvalues_check: no possible values\n");
result = 0LL;
}
else
{
v2 = 0LL;
v3 = (__int64)&a1[(unsigned int)(a2 - 1) + 1];
do
{
if ( *a1 )
{
if ( v2 )
return 0LL;
v2 = *a1;
}
++a1;
}
while ( a1 != (__int64 *)v3 );
if ( !v2 )
goto LABEL_10;
result = v2;
}
return result;
}

canonical_decompiled_code:
__int64 __fastcall func1(__int64 *a1, int a2)
{
__int64 v2; // r8
__int64 v3; // rdx
__int64 result; // rax

if ( a2 <= 0 )
{
LABEL_10:
fatal_error("pvalues_check: no possible values\n");
result = 0LL;
}
else
{
v2 = 0LL;
v3 = (__int64)&a1[(unsigned int)(a2 - 1) + 1];
do
{
if ( *a1 )
{
if ( v2 )
return 0LL;
v2 = *a1;
}
++a1;
}
while ( a1 != (__int64 *)v3 );
if ( !v2 )
goto LABEL_10;
result = v2;
}
return result;
}

original_code:
static
Term pvalues_check(Term *a, int n)
{
  Term b = ((void *)0);
  int i;
  for (i = 0; i < n; i++) {
    if (a[i] != ((void *)0)) {
      if (b != ((void *)0))
 return ((void *)0);
      else
 b = a[i];
    }
  }
  if (b == ((void *)0))
    fatal_error("pvalues_check: no possible values\n");
  return b;
}

canonical_original_code:
static struct term *pvalues_check(struct term **a, int n)
{
  struct term *b = ((void *)0);
  int i;
  for (i = 0; i < n; i++) {
    if (a[i] != ((void *)0)) {
      if (b != ((void *)0))
 return ((void *)0);
      else
 b = a[i];
    }
  }
  if (b == ((void *)0))
    fatal_error("pvalues_check: no possible values\n");
  return b;
}

variable_types:
a
struct term **

variable_types: n int

variable_types: struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *

variable_types: i int


eterm

decompiled_code:
__int64 __fastcall eterm(__int64 a1, _DWORD *a2)
{
int v4; // esi
__int64 v5; // rdx
int v6; // ecx
int v7; // eax
int v8; // eax

*a2 = -1;
if ( !a1 )
return 0LL;
if ( *(int *)a1 < 0 && !(unsigned int)arith_rel_term() && !(unsigned int)arith_op_term(a1) )
{
v4 = *(_DWORD *)(*(_QWORD *)(Sn_to_mace_sn + 8LL * -*(_DWORD *)a1) + 16LL);
LODWORD(v5) = *(unsigned __int8 *)(a1 + 4) - 1;
if ( !*(_BYTE *)(a1 + 4) )
{
LABEL_13:
*a2 = v4;
return 1LL;
}
v5 = (int)v5;
v6 = 1;
while ( 1 )
{
v8 = **(_DWORD **)(*(_QWORD *)(a1 + 8) + 8 * v5);
if ( v8 < 0 )
break;
v7 = v6 * v8;
--v5;
v6 *= Domain_size;
v4 += v7;
if ( (_DWORD)v5 == -1 )
goto LABEL_13;
}
}
return 0LL;
}

canonical_decompiled_code:
__int64 __fastcall func3(__int64 a1, _DWORD *a2)
{
int v4; // esi
__int64 v5; // rdx
int v6; // ecx
int v7; // eax
int v8; // eax

*a2 = -1;
if ( !a1 )
return 0LL;
if ( *(int *)a1 < 0 && !(unsigned int)arith_rel_term() && !(unsigned int)arith_op_term(a1) )
{
v4 = *(_DWORD *)(*(_QWORD *)(Sn_to_mace_sn + 8LL * -*(_DWORD *)a1) + 16LL);
LODWORD(v5) = *(unsigned __int8 *)(a1 + 4) - 1;
if ( !*(_BYTE *)(a1 + 4) )
{
LABEL_13:
*a2 = v4;
return 1LL;
}
v5 = (int)v5;
v6 = 1;
while ( 1 )
{
v8 = **(_DWORD **)(*(_QWORD *)(a1 + 8) + 8 * v5);
if ( v8 < 0 )
break;
v7 = v6 * v8;
--v5;
v6 *= Domain_size;
v4 += v7;
if ( (_DWORD)v5 == -1 )
goto LABEL_13;
}
}
return 0LL;
}

original_code:
BOOL eterm(Term t, int *pid)
{
  *pid = -1;
  if (t == ((void *)0) || ((t)->private_symbol >= 0) || arith_rel_term(t) || arith_op_term(t))
    return FALSE;
  else {
    int i;
    int mult = 1;
    int id = Sn_to_mace_sn[(-((t)->private_symbol))]->base;
    for (i = ((t)->arity)-1; i >= 0; i--) {
      if (!((((t)->args[i]))->private_symbol >= 0))
        return FALSE;
      else
        id += ((((t)->args[i]))->private_symbol) * mult;
      mult *= Domain_size;
    }
    *pid = id;
    return TRUE;
  }
}

canonical_original_code:
enum BOOL eterm(struct term *t, int *pid)
{
  *pid = -1;
  if (t == ((void *)0) || ((t)->private_symbol >= 0) || arith_rel_term(t) || arith_op_term(t))
    return FALSE;
  else {
    int i;
    int mult = 1;
    int id = Sn_to_mace_sn[(-((t)->private_symbol))]->base;
    for (i = ((t)->arity)-1; i >= 0; i--) {
      if (!((((t)->args[i]))->private_symbol >= 0))
        return FALSE;
      else
        id += ((((t)->args[i]))->private_symbol) * mult;
      mult *= Domain_size;
    }
    *pid = id;
    return TRUE;
  }
}

variable_types:
pid
int *

variable_types: mult int

return_type: enum BOOL { FALSE=0, TRUE=1 }

user_defined_types: struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; }


decompiled_code:
__int64 __fastcall decode_eterm_id(int a1)
{
unsigned int *v1; // rbp
__int64 v2; // rax
unsigned int v3; // er12
__int64 v4; // r14
int v5; // ebx
int v6; // er13
int v7; // er8
__int64 v8; // rax

v1 = *(unsigned int **)(Cells + 56LL * a1 + 48);
v2 = get_rigid_term_dangerously(*v1, v1[2]);
v3 = Domain_size;
v4 = v2;
v5 = a1 - v1[4];
v6 = v1[2] - 1;
if ( v6 >= 0 )
{
do
{
v7 = int_power(v3, (unsigned int)v6);
v8 = v5 / v7;
v5 %= v7;
*(_QWORD *)(*(_QWORD *)(v4 + 8) + 8LL * (int)(v1[2] + ~v6)) = *(_QWORD *)(Domain + 8 * v8);
}
while ( v6-- != 0 );
}
return v4;
}

canonical_decompiled_code:
__int64 __fastcall func4(int a1)
{
unsigned int *v1; // rbp
__int64 v2; // rax
unsigned int v3; // er12
__int64 v4; // r14
int v5; // ebx
int v6; // er13
int v7; // er8
__int64 v8; // rax

v1 = *(unsigned int **)(Cells + 56LL * a1 + 48);
v2 = get_rigid_term_dangerously(*v1, v1[2]);
v3 = Domain_size;
v4 = v2;
v5 = a1 - v1[4];
v6 = v1[2] - 1;
if ( v6 >= 0 )
{
do
{
v7 = int_power(v3, (unsigned int)v6);
v8 = v5 / v7;
v5 %= v7;
*(_QWORD *)(*(_QWORD *)(v4 + 8) + 8LL * (int)(v1[2] + ~v6)) = *(_QWORD *)(Domain + 8 * v8);
}
while ( v6-- != 0 );
}
return v4;
}

original_code:
Term decode_eterm_id(int id)
{
  Symbol_data s = Cells[id].symbol;
  Term t = get_rigid_term_dangerously(s->sn, s->arity);
  int n = Domain_size;
  int x = id - s->base;
  int i;
  for (i = s->arity - 1; i >= 0; i--) {
    int p = int_power(n, i);
    int e = x / p;
    ((t)->args[(s->arity-1) - i]) = Domain[e];
    x = x % p;
  }
  return t;
}

canonical_original_code:
struct term *decode_eterm_id(int id)
{
  struct symbol_data *s = Cells[id].symbol;
  struct term *t = get_rigid_term_dangerously(s->sn, s->arity);
  int n = Domain_size;
  int x = id - s->base;
  int i;
  for (i = s->arity - 1; i >= 0; i--) {
    int p = int_power(n, i);
    int e = x / p;
    ((t)->args[(s->arity-1) - i]) = Domain[e];
    x = x % p;
  }
  return t;
}

variable_types: struct symbol_data { int sn; int mace_sn; int arity; int type; int base; int attribute; struct symbol_data *next; } *

variable_types: x int

variable_types: p int

variable_types: e int

return_type: struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *


decompiled_code:
__int64 init_standard_options()
{
__int64 result; // rax

Prolog_style_variables = init_flag("prolog_style_variables", 0LL);
init_flag("ignore_option_dependencies", 0LL);
result = init_flag("clocks", 0LL);
Clocks = result;
return result;
}

canonical_decompiled_code:
__int64 func0()
{
__int64 result; // rax

Prolog_style_variables = init_flag("prolog_style_variables", 0LL);
init_flag("ignore_option_dependencies", 0LL);
result = init_flag("clocks", 0LL);
Clocks = result;
return result;
}

original_code:
void init_standard_options(void)
{
  Prolog_style_variables = init_flag("prolog_style_variables", FALSE);
  Ignore_option_dependencies = init_flag("ignore_option_dependencies", FALSE);
  Clocks = init_flag("clocks", FALSE);
}

canonical_original_code:
void init_standard_options()
{
  Prolog_style_variables = init_flag("prolog_style_variables", FALSE);
  Ignore_option_dependencies = init_flag("ignore_option_dependencies", FALSE);
  Clocks = init_flag("clocks", FALSE);
}


decompiled_code:
__int64 process_standard_options()
{
if ( (unsigned int)flag((unsigned int)Clocks) )
{
enable_clocks();
if ( (unsigned int)flag((unsigned int)Prolog_style_variables) )
return set_variable_style(1LL);
}
else
{
disable_clocks();
if ( (unsigned int)flag((unsigned int)Prolog_style_variables) )
return set_variable_style(1LL);
}
return set_variable_style(0LL);
}

canonical_decompiled_code:
__int64 func1()
{
if ( (unsigned int)flag((unsigned int)Clocks) )
{
enable_clocks();
if ( (unsigned int)flag((unsigned int)Prolog_style_variables) )
return set_variable_style(1LL);
}
else
{
disable_clocks();
if ( (unsigned int)flag((unsigned int)Prolog_style_variables) )
return set_variable_style(1LL);
}
return set_variable_style(0LL);
}

original_code:
void process_standard_options(void)
{
  if (flag(Clocks))
    enable_clocks();
  else
    disable_clocks();
  if (flag(Prolog_style_variables))
    set_variable_style(PROLOG_STYLE);
  else
    set_variable_style(STANDARD_STYLE);
}

canonical_original_code:
void process_standard_options()
{
  if (flag(Clocks))
    enable_clocks();
  else
    disable_clocks();
  if (flag(Prolog_style_variables))
    set_variable_style(PROLOG_STYLE);
  else
    set_variable_style(STANDARD_STYLE);
}


decompiled_code:
__int64 clocks_id()
{
return (unsigned int)Clocks;
}

canonical_decompiled_code:
__int64 func2()
{
return (unsigned int)Clocks;
}

original_code:
int clocks_id(void)
{
  return Clocks;
}

canonical_original_code:
int clocks_id()
{
  return Clocks;
}


decompiled_code:
__int64 prolog_style_variables_id()
{
return (unsigned int)Prolog_style_variables;
}

canonical_decompiled_code:
__int64 func3()
{
return (unsigned int)Prolog_style_variables;
}

original_code:
int prolog_style_variables_id(void)
{
  return Prolog_style_variables;
}

canonical_original_code:
int prolog_style_variables_id()
{
  return Prolog_style_variables;
}


decompiled_code:
unsigned int *__fastcall vars_to_names(unsigned int *a1)
{
__int64 v1; // rbx
_QWORD *v2; // r12
unsigned int *result; // rax
char *v4; // r12
void *v5; // r13
int v6; // ebx
const char *v7; // rax
char *v8; // r13
char *v9; // r14
__int64 v10; // r12

if ( (*a1 & 0x80000000) == 0 )
{
v4 = (char *)malloc(0x19uLL);
v5 = malloc(0x19uLL);
v6 = variable_style();
v7 = (const char *)int_to_str(*a1, v5, 25LL);
v8 = (char *)v7;
switch ( v6 )
{
case 1:
strcpy(v4, "VAR_");
break;
case 2:
*v4 = 0;
break;
case 0:
strcpy(v4, "var_");
break;
}
v9 = v4;
strcat(v4, v7);
v10 = get_rigid_term(v4, 0LL);
free_term(a1);
free(v9);
free(v8);
result = (unsigned int *)v10;
}
else
{
v1 = 0LL;
if ( *((_BYTE *)a1 + 4) )
{
do
{
v2 = (_QWORD *)(*((_QWORD *)a1 + 1) + 8 * v1++);
*v2 = vars_to_names(*v2);
}
while ( *((unsigned __int8 *)a1 + 4) > (int)v1 );
}
result = a1;
}
return result;
}

canonical_decompiled_code:
unsigned int *__fastcall func0(unsigned int *a1)
{
__int64 v1; // rbx
_QWORD *v2; // r12
unsigned int *result; // rax
char *v4; // r12
void *v5; // r13
int v6; // ebx
const char *v7; // rax
char *v8; // r13
char *v9; // r14
__int64 v10; // r12

if ( (*a1 & 0x80000000) == 0 )
{
v4 = (char *)malloc(0x19uLL);
v5 = malloc(0x19uLL);
v6 = variable_style();
v7 = (const char *)int_to_str(*a1, v5, 25LL);
v8 = (char *)v7;
switch ( v6 )
{
case 1:
strcpy(v4, "VAR_");
break;
case 2:
*v4 = 0;
break;
case 0:
strcpy(v4, "var_");
break;
}
v9 = v4;
strcat(v4, v7);
v10 = get_rigid_term(v4, 0LL);
free_term(a1);
free(v9);
free(v8);
result = (unsigned int *)v10;
}
else
{
v1 = 0LL;
if ( *((_BYTE *)a1 + 4) )
{
do
{
v2 = (_QWORD *)(*((_QWORD *)a1 + 1) + 8 * v1++);
*v2 = func0(*v2);
}
while ( *((unsigned __int8 *)a1 + 4) > (int)v1 );
}
result = a1;
}
return result;
}

original_code:
static
Term vars_to_names(Term t)
{
  if (((t)->private_symbol >= 0)) {
    Term a;
    char *s1 = malloc(25);
    char *s2 = malloc(25);
    Variable_style v = variable_style();
    s2 = int_to_str(((t)->private_symbol), s2, 25);
    switch (v) {
    case INTEGER_STYLE: s1 = strcpy(s1, ""); break;
    case STANDARD_STYLE: s1 = strcpy(s1, "var_"); break;
    case PROLOG_STYLE: s1 = strcpy(s1, "VAR_"); break;
    }
    s1 = strcat(s1, s2);
    a = get_rigid_term(s1, 0);
    free_term(t);
    free(s1);
    free(s2);
    return a;
  }
  else {
    int i;
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = vars_to_names(((t)->args[i]));
    return t;
  }
}

canonical_original_code:
static struct term *vars_to_names(struct term *t)
{
  if (((t)->private_symbol >= 0)) {
    struct term *a;
    char *s1 = malloc(25);
    char *s2 = malloc(25);
    enum Variable_style v = variable_style();
    s2 = int_to_str(((t)->private_symbol), s2, 25);
    switch (v) {
    case INTEGER_STYLE: s1 = strcpy(s1, ""); break;
    case STANDARD_STYLE: s1 = strcpy(s1, "var_"); break;
    case PROLOG_STYLE: s1 = strcpy(s1, "VAR_"); break;
    }
    s1 = strcat(s1, s2);
    a = get_rigid_term(s1, 0);
    free_term(t);
    free(s1);
    free(s2);
    return a;
  }
  else {
    int i;
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = vars_to_names(((t)->args[i]));
    return t;
  }
}

variable_types:
t
struct term *

variable_types: enum Variable_style { STANDARD_STYLE=0, PROLOG_STYLE=1, INTEGER_STYLE=2 }


decompiled_code:
__int64 __fastcall zap_tlist(_QWORD *a1)
{
__int64 result; // rax

if ( a1 )
{
zap_tlist(a1[1]);
zap_term(*a1);
result = free_plist(a1);
}
return result;
}

canonical_decompiled_code:
__int64 __fastcall func0(_QWORD *a1)
{
__int64 result; // rax

if ( a1 )
{
func0(a1[1]);
zap_term(*a1);
result = free_plist(a1);
}
return result;
}

original_code:
void zap_tlist(Plist p)
{
  if (p != ((void *)0)) {
    zap_tlist(p->next);
    zap_term(p->v);
    free_plist(p);
  }
}

canonical_original_code:
void zap_tlist(struct plist *p)
{
  if (p != ((void *)0)) {
    zap_tlist(p->next);
    zap_term(p->v);
    free_plist(p);
  }
}

user_defined_types: struct plist { void *v; struct plist *next; }


decompiled_code:
__int64 __fastcall constants_in_term(__int64 a1, __int64 a2)
{
__int64 v2; // rbp
__int64 v3; // r12
__int64 v5; // rdi

v2 = a2;
if ( *(int *)a1 >= 0 )
return v2;
v3 = 0LL;
if ( *(_BYTE *)(a1 + 4) )
{
do
{
v5 = *(_QWORD *)(*(_QWORD *)(a1 + 8) + 8 * v3++);
v2 = constants_in_term(v5, v2);
}
while ( *(unsigned __int8 *)(a1 + 4) > (int)v3 );
return v2;
}
if ( (unsigned int)ilist_member(a2, (unsigned int)-*(_DWORD *)a1) )
return v2;
return ilist_prepend(a2, (unsigned int)-*(_DWORD *)a1);
}

canonical_decompiled_code:
__int64 __fastcall func1(__int64 a1, __int64 a2)
{
__int64 v2; // rbp
__int64 v3; // r12
__int64 v5; // rdi

v2 = a2;
if ( *(int *)a1 >= 0 )
return v2;
v3 = 0LL;
if ( *(_BYTE *)(a1 + 4) )
{
do
{
v5 = *(_QWORD *)(*(_QWORD *)(a1 + 8) + 8 * v3++);
v2 = func1(v5, v2);
}
while ( *(unsigned __int8 *)(a1 + 4) > (int)v3 );
return v2;
}
if ( (unsigned int)ilist_member(a2, (unsigned int)-*(_DWORD *)a1) )
return v2;
return ilist_prepend(a2, (unsigned int)-*(_DWORD *)a1);
}

original_code:
Ilist constants_in_term(Term t, Ilist p)
{
  if (((t)->private_symbol >= 0))
    return p;
  else if (((t)->private_symbol < 0 && (t)->arity == 0)) {
    if (ilist_member(p, (-((t)->private_symbol))))
      return p;
    else
      return ilist_prepend(p, (-((t)->private_symbol)));
  }
  else {
    int i;
    for (i = 0; i < ((t)->arity); i++)
      p = constants_in_term(((t)->args[i]), p);
    return p;
  }
}

canonical_original_code:
struct ilist *constants_in_term(struct term *t, struct ilist *p)
{
  if (((t)->private_symbol >= 0))
    return p;
  else if (((t)->private_symbol < 0 && (t)->arity == 0)) {
    if (ilist_member(p, (-((t)->private_symbol))))
      return p;
    else
      return ilist_prepend(p, (-((t)->private_symbol)));
  }
  else {
    int i;
    for (i = 0; i < ((t)->arity); i++)
      p = constants_in_term(((t)->args[i]), p);
    return p;
  }
}

variable_types:
p
struct ilist *

return_type: struct ilist { int i; struct ilist *next; } *


decompiled_code:
int p_clash_mem()
{
return fprint_clash_mem(stdout, 1);
}

canonical_decompiled_code:
int func4()
{
return func3(stdout, 1);
}

original_code:
void p_clash_mem()
{
  fprint_clash_mem(stdout, TRUE);
}


decompiled_code:
__int64 __fastcall apply_lit(unsigned int *a1)
{
__int64 v1; // rax

v1 = apply(*((_QWORD *)a1 + 1));
return new_literal(*a1, v1);
}

canonical_decompiled_code:
__int64 __fastcall func7(unsigned int *a1)
{
__int64 v1; // rax

v1 = apply(*((_QWORD *)a1 + 1));
return new_literal(*a1, v1);
}

original_code:
Literals apply_lit(Literals lit, Context c)
{
  return new_literal(lit->sign, apply(lit->atom, c));
}

canonical_original_code:
struct literals *apply_lit(struct literals *lit, struct context *c)
{
  return new_literal(lit->sign, apply(lit->atom, c));
}

variable_types:
lit
struct literals *

variable_types: struct context { struct term *terms[100]; struct context *contexts[100]; int multiplier; struct term *partial_term; } *

return_type: struct literals { enum BOOL { FALSE=0, TRUE=1 } sign; struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *atom; struct literals *next; } *

user_defined_types: struct literals { enum BOOL sign; struct term *atom; struct literals *next; }


original_code:
void merge_sort_recurse(void *a[],
   void *w[],
   int start,
   int end,
   Ordertype (*comp_proc) (void *, void *))
{
  int mid, i, i1, i2, e1, e2;
  if (start < end) {
    mid = (start+end)/2;
    merge_sort_recurse(a, w, start, mid, comp_proc);
    merge_sort_recurse(a, w, mid+1, end, comp_proc);
    i1 = start; e1 = mid;
    i2 = mid+1; e2 = end;
    i = start;
    while (i1 <= e1 && i2 <= e2) {
      if ((*comp_proc)(a[i1], a[i2]) == GREATER_THAN)
 w[i++] = a[i2++];
      else
 w[i++] = a[i1++];
    }
    if (i2 > e2)
      while (i1 <= e1)
 w[i++] = a[i1++];
    else
      while (i2 <= e2)
 w[i++] = a[i2++];
    for (i = start; i <= end; i++)
      a[i] = w[i];
  }
}

canonical_original_code:
void merge_sort_recurse(void *a[], void *w[], int start, int end, enum Ordertype (*comp_proc)(void *, void *))
{
  int mid; int i; int i1; int i2; int e1; int e2;
  if (start < end) {
    mid = (start+end)/2;
    merge_sort_recurse(a, w, start, mid, comp_proc);
    merge_sort_recurse(a, w, mid+1, end, comp_proc);
    i1 = start; e1 = mid;
    i2 = mid+1; e2 = end;
    i = start;
    while (i1 <= e1 && i2 <= e2) {
      if ((*comp_proc)(a[i1], a[i2]) == GREATER_THAN)
 w[i++] = a[i2++];
      else
 w[i++] = a[i1++];
    }
    if (i2 > e2)
      while (i1 <= e1)
 w[i++] = a[i1++];
    else
      while (i2 <= e2)
 w[i++] = a[i2++];
    for (i = start; i <= end; i++)
      a[i] = w[i];
  }
}

variable_types:
a
void *[]

variable_types:
w
void *[]

variable_types: start int

variable_types: end int

variable_types: enum Ordertype { NOT_COMPARABLE=0, SAME_AS=1, LESS_THAN=2, GREATER_THAN=3, LESS_THAN_OR_SAME_AS=4, GREATER_THAN_OR_SAME_AS=5, NOT_LESS_THAN=6, NOT_GREATER_THAN=7 } (*)(void *, void *)

variable_types: mid int


decompiled_code:
void __fastcall merge_sort(__int64 a1, int a2, unsigned int (__fastcall *a3)(_QWORD, _QWORD))
{
void *v4; // rbp

v4 = malloc(8LL * a2);
merge_sort_recurse(a1, (__int64)v4, 0, a2 - 1, a3);
free(v4);
}

canonical_decompiled_code:
void __fastcall func1(__int64 a1, int a2, unsigned int (__fastcall *a3)(_QWORD, _QWORD))
{
void *v4; // rbp

v4 = malloc(8LL * a2);
func0(a1, (__int64)v4, 0, a2 - 1, a3);
free(v4);
}

original_code:
void merge_sort(void *a[],
  int n,
  Ordertype (*comp_proc) (void *, void *))
{
  void **work = malloc(n * sizeof(void *));
  merge_sort_recurse((void **) a, work, 0, n-1, comp_proc);
  free(work);
}

canonical_original_code:
void merge_sort(void *a[], int n, enum Ordertype (*comp_proc)(void *, void *))
{
  void **work = malloc(n * sizeof(void *));
  merge_sort_recurse((void **) a, work, 0, n-1, comp_proc);
  free(work);
}

variable_types: n int

variable_types:
work
void **

user_defined_types: enum Ordertype { NOT_COMPARABLE=0, SAME_AS=1, LESS_THAN=2, GREATER_THAN=3, LESS_THAN_OR_SAME_AS=4, GREATER_THAN_OR_SAME_AS=5, NOT_LESS_THAN=6, NOT_GREATER_THAN=7 }


decompiled_code:
__int64 __fastcall compare_vecs(__int64 a1, __int64 a2, int a3)
{
__int64 v3; // rax
int v4; // ecx

if ( a3 <= 0 )
return 1LL;
v3 = 0LL;
while ( 1 )
{
v4 = *(_DWORD *)(a2 + 4 * v3);
if ( *(_DWORD *)(a1 + 4 * v3) < v4 )
return 2LL;
if ( *(_DWORD *)(a1 + 4 * v3) > v4 )
break;
if ( ++v3 == a3 )
return 1LL;
}
return 3LL;
}

canonical_decompiled_code:
__int64 __fastcall func2(__int64 a1, __int64 a2, int a3)
{
__int64 v3; // rax
int v4; // ecx

if ( a3 <= 0 )
return 1LL;
v3 = 0LL;
while ( 1 )
{
v4 = *(_DWORD *)(a2 + 4 * v3);
if ( *(_DWORD *)(a1 + 4 * v3) < v4 )
return 2LL;
if ( *(_DWORD *)(a1 + 4 * v3) > v4 )
break;
if ( ++v3 == a3 )
return 1LL;
}
return 3LL;
}

canonical_original_code:
enum Ordertype compare_vecs(int *a, int *b, int n)
{
  int i;
  for (i = 0; i < n; i++) {
    if (a[i] < b[i])
      return LESS_THAN;
    else if (a[i] > b[i])
      return GREATER_THAN;
  }
  return SAME_AS;
}

variable_types:
a
int *

variable_types:
b
int *

variable_types: i int

return_type: enum Ordertype { NOT_COMPARABLE=0, SAME_AS=1, LESS_THAN=2, GREATER_THAN=3, LESS_THAN_OR_SAME_AS=4, GREATER_THAN_OR_SAME_AS=5, NOT_LESS_THAN=6, NOT_GREATER_THAN=7 }


original_code:
void copy_vec(int *a, int *b, int n)
{
  int i;
  for (i = 0; i < n; i++)
    b[i] = a[i];
}


decompiled_code:
int p_flatterm_mem()
{
return fprint_flatterm_mem(stdout, 1);
}

canonical_decompiled_code:
int func3()
{
return func2(stdout, 1);
}

original_code:
void p_flatterm_mem()
{
  fprint_flatterm_mem(stdout, TRUE);
}


decompiled_code:
__int64 get_jnode()
{
__int64 result; // rax

result = get_mem(6LL);
++Jnode_gets;
return result;
}

canonical_decompiled_code:
__int64 func2()
{
__int64 result; // rax

result = get_mem(6LL);
++Jnode_gets;
return result;
}

original_code:
Jnode get_jnode(void)
{
  Jnode p = get_mem(((sizeof(struct jnode))%(sizeof(void *)) == 0 ? (sizeof(struct jnode))/(sizeof(void *)) : (sizeof(struct jnode))/(sizeof(void *)) + 1));
  Jnode_gets++;
  return(p);
}

canonical_original_code:
struct jnode *get_jnode()
{
  struct jnode *p = get_mem(((sizeof(struct jnode))%(sizeof(void *)) == 0 ? (sizeof(struct jnode))/(sizeof(void *)) : (sizeof(struct jnode))/(sizeof(void *)) + 1));
  Jnode_gets++;
  return(p);
}

variable_types: struct jnode { int type; int id; struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *alpha; struct term *beta; int pos; struct jnode *prev; struct jnode *next; } *

user_defined_types: struct jnode { int type; int id; struct term *alpha; struct term *beta; int pos; struct jnode *prev; struct jnode *next; }


decompiled_code:
__int64 __fastcall free_jnode(__int64 a1)
{
__int64 result; // rax

result = free_mem(a1, 6LL);
++Jnode_frees;
return result;
}

canonical_decompiled_code:
__int64 __fastcall func3(__int64 a1)
{
__int64 result; // rax

result = free_mem(a1, 6LL);
++Jnode_frees;
return result;
}

original_code:
void free_jnode(Jnode p)
{
  free_mem(p, ((sizeof(struct jnode))%(sizeof(void *)) == 0 ? (sizeof(struct jnode))/(sizeof(void *)) : (sizeof(struct jnode))/(sizeof(void *)) + 1));
  Jnode_frees++;
}

canonical_original_code:
void free_jnode(struct jnode *p)
{
  free_mem(p, ((sizeof(struct jnode))%(sizeof(void *)) == 0 ? (sizeof(struct jnode))/(sizeof(void *)) : (sizeof(struct jnode))/(sizeof(void *)) + 1));
  Jnode_frees++;
}


decompiled_code:
int p_mstate_mem()
{
return fprint_mstate_mem(stdout, 1);
}

canonical_decompiled_code:
int func5()
{
return func4(stdout, 1);
}

original_code:
void p_mstate_mem()
{
  fprint_mstate_mem(stdout, TRUE);
}


decompiled_code:
__int64 next_clause_id()
{
return (unsigned int)++Topform_id_count;
}

canonical_decompiled_code:
__int64 func0()
{
return (unsigned int)++Topform_id_count;
}

original_code:
static
int next_clause_id(void)
{
  return ++Topform_id_count;
}

canonical_original_code:
static int next_clause_id()
{
  return ++Topform_id_count;
}


decompiled_code:
__int64 clause_ids_assigned()
{
return (unsigned int)Topform_id_count;
}

canonical_decompiled_code:
__int64 func1()
{
return (unsigned int)Topform_id_count;
}

original_code:
int clause_ids_assigned(void)
{
  return Topform_id_count;
}

canonical_original_code:
int clause_ids_assigned()
{
  return Topform_id_count;
}


decompiled_code:
int p_clause_id_tab()
{
return fprint_clause_id_tab(stdout);
}

canonical_decompiled_code:
int func4()
{
return func3(stdout);
}

original_code:
void p_clause_id_tab()
{
  fprint_clause_id_tab(stdout);
}


decompiled_code:
__int64 __fastcall fast_parse(__int64 a1)
{
char v1; // al
__int64 v2; // r12
__int64 v4; // rdi
__int64 v5; // r13
__int64 v6; // rbx
_QWORD *v7; // r14
__int64 result; // rax
unsigned int v9; // eax
char v10[42]; // [rsp+0h] [rbp-2Ah] BYREF

v1 = *(_BYTE *)(a1 + Pos++);
if ( (unsigned __int8)(v1 - 114) > 8u )
{
v2 = v1;
v4 = (unsigned int)Symnum[v1];
if ( !(_DWORD)v4 )
{
v10[0] = v1;
v10[1] = 0;
v9 = str_to_sn(v10, 0LL);
Symnum[v2] = v9;
v4 = v9;
}
v5 = get_rigid_term_dangerously(v4, (unsigned int)Arity[v2]);
if ( Arity[v2] > 0 )
{
v6 = 0LL;
do
{
v7 = (_QWORD *)(*(_QWORD *)(v5 + 8) + 8 * v6++);
*v7 = fast_parse(a1);
}
while ( Arity[v2] > (int)v6 );
}
result = v5;
}
else
{
switch ( v1 )
{
case 's':
result = get_variable_term(7LL);
break;
case 't':
result = get_variable_term(6LL);
break;
case 'u':
result = get_variable_term(5LL);
break;
case 'v':
result = get_variable_term(4LL);
break;
case 'w':
result = get_variable_term(3LL);
break;
case 'x':
result = get_variable_term(2LL);
break;
case 'y':
result = get_variable_term(1LL);
break;
case 'z':
result = get_variable_term(0LL);
break;
default:
result = get_variable_term(8LL);
break;
}
}
return result;
}

canonical_decompiled_code:
__int64 __fastcall func0(__int64 a1)
{
char v1; // al
__int64 v2; // r12
__int64 v4; // rdi
__int64 v5; // r13
__int64 v6; // rbx
_QWORD *v7; // r14
__int64 result; // rax
unsigned int v9; // eax
char v10[42]; // [rsp+0h] [rbp-2Ah] BYREF

v1 = *(_BYTE *)(a1 + Pos++);
if ( (unsigned __int8)(v1 - 114) > 8u )
{
v2 = v1;
v4 = (unsigned int)Symnum[v1];
if ( !(_DWORD)v4 )
{
v10[0] = v1;
v10[1] = 0;
v9 = str_to_sn(v10, 0LL);
Symnum[v2] = v9;
v4 = v9;
}
v5 = get_rigid_term_dangerously(v4, (unsigned int)Arity[v2]);
if ( Arity[v2] > 0 )
{
v6 = 0LL;
do
{
v7 = (_QWORD *)(*(_QWORD *)(v5 + 8) + 8 * v6++);
*v7 = func0(a1);
}
while ( Arity[v2] > (int)v6 );
}
result = v5;
}
else
{
switch ( v1 )
{
case 's':
result = get_variable_term(7LL);
break;
case 't':
result = get_variable_term(6LL);
break;
case 'u':
result = get_variable_term(5LL);
break;
case 'v':
result = get_variable_term(4LL);
break;
case 'w':
result = get_variable_term(3LL);
break;
case 'x':
result = get_variable_term(2LL);
break;
case 'y':
result = get_variable_term(1LL);
break;
case 'z':
result = get_variable_term(0LL);
break;
default:
result = get_variable_term(8LL);
break;
}
}
return result;
}

original_code:
static
Term fast_parse(char *s)
{
  char c = s[Pos++];
  Term t;
  if (c >= 'r' && c <= 'z') {
    switch (c) {
    case 'z': t = get_variable_term(0); break;
    case 'y': t = get_variable_term(1); break;
    case 'x': t = get_variable_term(2); break;
    case 'w': t = get_variable_term(3); break;
    case 'v': t = get_variable_term(4); break;
    case 'u': t = get_variable_term(5); break;
    case 't': t = get_variable_term(6); break;
    case 's': t = get_variable_term(7); break;
    case 'r': t = get_variable_term(8); break;
    default: t = ((void *)0);
    }
    return t;
  }
  else {
    int i;
    if (Symnum[(int) c] == 0) {
      char str[2];
      str[0] = c; str[1] = '\0';
      Symnum[(int) c] = str_to_sn(str, 0);
    }
    t = get_rigid_term_dangerously(Symnum[(int) c], Arity[(int) c]);
    for (i = 0; i < Arity[(int) c]; i++) {
      ((t)->args[i]) = fast_parse(s);
    }
    return t;
  }
}

canonical_original_code:
static struct term *fast_parse(char *s)
{
  char c = s[Pos++];
  struct term *t;
  if (c >= 'r' && c <= 'z') {
    switch (c) {
    case 'z': t = get_variable_term(0); break;
    case 'y': t = get_variable_term(1); break;
    case 'x': t = get_variable_term(2); break;
    case 'w': t = get_variable_term(3); break;
    case 'v': t = get_variable_term(4); break;
    case 'u': t = get_variable_term(5); break;
    case 't': t = get_variable_term(6); break;
    case 's': t = get_variable_term(7); break;
    case 'r': t = get_variable_term(8); break;
    default: t = ((void *)0);
    }
    return t;
  }
  else {
    int i;
    if (Symnum[(int) c] == 0) {
      char str[2];
      str[0] = c; str[1] = '\0';
      Symnum[(int) c] = str_to_sn(str, 0);
    }
    t = get_rigid_term_dangerously(Symnum[(int) c], Arity[(int) c]);
    for (i = 0; i < Arity[(int) c]; i++) {
      ((t)->args[i]) = fast_parse(s);
    }
    return t;
  }
}

variable_types:
s
char *

variable_types: c char

variable_types: struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *

variable_types:
str
char [2]


decompiled_code:
__int64 __fastcall fast_set_symbol(char a1, __int64 a2)
{
__int64 result; // rax
char v3[10]; // [rsp+0h] [rbp-Ah] BYREF

if ( (unsigned __int8)(a1 - 114) <= 8u )
return fatal_error("fast_set_symbol, r--z are variables and cannot be declared");
Arity[a1] = a2;
v3[0] = a1;
v3[1] = 0;
result = str_to_sn(v3, a2);
Symnum[a1] = result;
return result;
}

canonical_decompiled_code:
__int64 __fastcall func2(char a1, __int64 a2)
{
__int64 result; // rax
char v3[10]; // [rsp+0h] [rbp-Ah] BYREF

if ( (unsigned __int8)(a1 - 114) <= 8u )
return fatal_error("fast_set_symbol, r--z are variables and cannot be declared");
Arity[a1] = a2;
v3[0] = a1;
v3[1] = 0;
result = str_to_sn(v3, a2);
Symnum[a1] = result;
return result;
}

original_code:
void fast_set_symbol(char c, int arity)
{
  if (c >= 'r' && c <= 'z') {
    fatal_error("fast_set_symbol, r--z are variables and cannot be declared");
  }
  else {
    char str[2];
    str[0] = c;
    str[1] = '\0';
    Arity[(int) c] = arity;
    Symnum[(int) c] = str_to_sn(str, arity);
  }
}

variable_types: arity int


decompiled_code:
__int64 fast_set_defaults()
{
fast_set_symbol(61, 2LL);
fast_set_symbol(109, 2LL);
fast_set_symbol(106, 2LL);
fast_set_symbol(102, 2LL);
fast_set_symbol(100, 2LL);
fast_set_symbol(42, 2LL);
fast_set_symbol(43, 2LL);
fast_set_symbol(47, 2LL);
fast_set_symbol(99, 1LL);
fast_set_symbol(103, 1LL);
fast_set_symbol(105, 1LL);
fast_set_symbol(45, 1LL);
fast_set_symbol(126, 1LL);
return fast_set_symbol(39, 1LL);
}

original_code:
void fast_set_defaults(void)
{
  fast_set_symbol('=', 2);
  fast_set_symbol('m', 2);
  fast_set_symbol('j', 2);
  fast_set_symbol('f', 2);
  fast_set_symbol('d', 2);
  fast_set_symbol('*', 2);
  fast_set_symbol('+', 2);
  fast_set_symbol('/', 2);
  fast_set_symbol('c', 1);
  fast_set_symbol('g', 1);
  fast_set_symbol('i', 1);
  fast_set_symbol('-', 1);
  fast_set_symbol('~', 1);
  fast_set_symbol('\'', 1);
}

canonical_original_code:
void fast_set_defaults()
{
  fast_set_symbol('=', 2);
  fast_set_symbol('m', 2);
  fast_set_symbol('j', 2);
  fast_set_symbol('f', 2);
  fast_set_symbol('d', 2);
  fast_set_symbol('*', 2);
  fast_set_symbol('+', 2);
  fast_set_symbol('/', 2);
  fast_set_symbol('c', 1);
  fast_set_symbol('g', 1);
  fast_set_symbol('i', 1);
  fast_set_symbol('-', 1);
  fast_set_symbol('~', 1);
  fast_set_symbol('\'', 1);
}


decompiled_code:
__int64 __fastcall free_clause_eval(__int64 a1)
{
__int64 result; // rax

result = free_mem(a1, 5LL);
++Clause_eval_frees;
return result;
}

canonical_decompiled_code:
__int64 __fastcall func0(__int64 a1)
{
__int64 result; // rax

result = free_mem(a1, 5LL);
++Clause_eval_frees;
return result;
}

original_code:
static
void free_clause_eval(Clause_eval p)
{
  free_mem(p, ((sizeof(struct clause_eval))%(sizeof(void *)) == 0 ? (sizeof(struct clause_eval))/(sizeof(void *)) : (sizeof(struct clause_eval))/(sizeof(void *)) + 1));
  Clause_eval_frees++;
}

canonical_original_code:
static void free_clause_eval(struct clause_eval *p)
{
  free_mem(p, ((sizeof(struct clause_eval))%(sizeof(void *)) == 0 ? (sizeof(struct clause_eval))/(sizeof(void *)) : (sizeof(struct clause_eval))/(sizeof(void *)) + 1));
  Clause_eval_frees++;
}

variable_types: struct clause_eval { int type; struct clause_eval *left; struct clause_eval *right; enum Ordertype { NOT_COMPARABLE=0, SAME_AS=1, LESS_THAN=2, GREATER_THAN=3, LESS_THAN_OR_SAME_AS=4, GREATER_THAN_OR_SAME_AS=5, NOT_LESS_THAN=6, NOT_GREATER_THAN=7 } relation; double test_val; } *

user_defined_types: struct clause_eval { int type; struct clause_eval *left; struct clause_eval *right; enum Ordertype relation; double test_val; }


decompiled_code:
__int64 get_clause_eval()
{
__int64 result; // rax

result = get_cmem(5LL);
++Clause_eval_gets;
return result;
}

canonical_decompiled_code:
__int64 func1()
{
__int64 result; // rax

result = get_cmem(5LL);
++Clause_eval_gets;
return result;
}

original_code:
static
Clause_eval get_clause_eval(void)
{
  Clause_eval p = get_cmem(((sizeof(struct clause_eval))%(sizeof(void *)) == 0 ? (sizeof(struct clause_eval))/(sizeof(void *)) : (sizeof(struct clause_eval))/(sizeof(void *)) + 1));
  Clause_eval_gets++;
  return(p);
}

canonical_original_code:
static struct clause_eval *get_clause_eval()
{
  struct clause_eval *p = get_cmem(((sizeof(struct clause_eval))%(sizeof(void *)) == 0 ? (sizeof(struct clause_eval))/(sizeof(void *)) : (sizeof(struct clause_eval))/(sizeof(void *)) + 1));
  Clause_eval_gets++;
  return(p);
}

return_type: struct clause_eval { int type; struct clause_eval *left; struct clause_eval *right; enum Ordertype { NOT_COMPARABLE=0, SAME_AS=1, LESS_THAN=2, GREATER_THAN=3, LESS_THAN_OR_SAME_AS=4, GREATER_THAN_OR_SAME_AS=5, NOT_LESS_THAN=6, NOT_GREATER_THAN=7 } relation; double test_val; } *


decompiled_code:
__int64 __fastcall zap_clause_eval_rule(__int64 a1)
{
if ( *(_DWORD *)a1 <= 1u )
{
zap_clause_eval_rule(*(_QWORD *)(a1 + 8));
zap_clause_eval_rule(*(_QWORD *)(a1 + 16));
}
return free_clause_eval(a1);
}

original_code:
void zap_clause_eval_rule(Clause_eval p)
{
  if (p->type == CL_EVAL_AND || p->type == CL_EVAL_OR) {
    zap_clause_eval_rule(p->left);
    zap_clause_eval_rule(p->right);
  }
  else if (p->type == CL_EVAL_OR)
    zap_clause_eval_rule(p->left);
  free_clause_eval(p);
}

canonical_original_code:
void zap_clause_eval_rule(struct clause_eval *p)
{
  if (p->type == CL_EVAL_AND || p->type == CL_EVAL_OR) {
    zap_clause_eval_rule(p->left);
    zap_clause_eval_rule(p->right);
  }
  else if (p->type == CL_EVAL_OR)
    zap_clause_eval_rule(p->left);
  free_clause_eval(p);
}


decompiled_code:
__int64 __fastcall compile_clause_eval_rule(__int64 a1)
{
__int64 v1; // r12
__int64 v2; // rax
__int64 v3; // rax
_QWORD *v5; // rax
__int64 v6; // rax
_QWORD *v7; // rax
__int64 v8; // r13
__int64 v9; // r14

v1 = get_clause_eval();
if ( (unsigned int)is_term(a1, asc_8F4, 2LL) )
{
*(_DWORD *)v1 = 0;
LABEL_3:
v2 = compile_clause_eval_rule(**(_QWORD **)(a1 + 8));
*(_QWORD *)(v1 + 8) = v2;
if ( v2 )
{
v3 = compile_clause_eval_rule(*(_QWORD *)(*(_QWORD *)(a1 + 8) + 8LL));
*(_QWORD *)(v1 + 16) = v3;
if ( v3 )
return v1;
}
return 0LL;
}
if ( (unsigned int)is_term(a1, &asc_8F4[1], 2LL) )
{
*(_DWORD *)v1 = 1;
goto LABEL_3;
}
if ( (unsigned int)is_term(a1, &asc_8F4[2], 1LL) )
{
v5 = *(_QWORD **)(a1 + 8);
*(_DWORD *)v1 = 2;
v6 = compile_clause_eval_rule(*v5);
*(_QWORD *)(v1 + 8) = v6;
if ( !v6 )
return 0LL;
return v1;
}
if ( (unsigned int)is_term(a1, "all", 0LL) )
{
*(_DWORD *)v1 = 3;
return v1;
}
if ( (unsigned int)is_term(a1, "positive", 0LL) )
{
*(_DWORD *)v1 = 9;
return v1;
}
if ( (unsigned int)is_term(a1, "negative", 0LL) )
{
*(_DWORD *)v1 = 10;
return v1;
}
if ( (unsigned int)is_term(a1, "mixed", 0LL) )
{
*(_DWORD *)v1 = 11;
return v1;
}
if ( (unsigned int)is_term(a1, "true", 0LL) )
{
*(_DWORD *)v1 = 13;
return v1;
}
if ( (unsigned int)is_term(a1, "false", 0LL) )
{
*(_DWORD *)v1 = 14;
return v1;
}
if ( (unsigned int)is_term(a1, "has_equality", 0LL) )
{
*(_DWORD *)v1 = 15;
return v1;
}
if ( (unsigned int)is_term(a1, "horn", 0LL) )
{
*(_DWORD *)v1 = 16;
return v1;
}
if ( (unsigned int)is_term(a1, "definite", 0LL) )
{
*(_DWORD *)v1 = 17;
return v1;
}
if ( (unsigned int)is_term(a1, "unit", 0LL) )
{
*(_DWORD *)v1 = 18;
return v1;
}
if ( (unsigned int)is_term(a1, "hint", 0LL) )
{
*(_DWORD *)v1 = 12;
return v1;
}
if ( (unsigned int)is_term(a1, "initial", 0LL) )
{
*(_DWORD *)v1 = 19;
return v1;
}
if ( (unsigned int)is_term(a1, "resolvent", 0LL) )
{
*(_DWORD *)v1 = 20;
return v1;
}
if ( (unsigned int)is_term(a1, "hyper_resolvent", 0LL) )
{
*(_DWORD *)v1 = 22;
return v1;
}
if ( (unsigned int)is_term(a1, "ur_resolvent", 0LL) )
{
*(_DWORD *)v1 = 21;
return v1;
}
if ( (unsigned int)is_term(a1, "factor", 0LL) )
{
*(_DWORD *)v1 = 23;
return v1;
}
if ( (unsigned int)is_term(a1, "paramodulant", 0LL) )
{
*(_DWORD *)v1 = 24;
return v1;
}
if ( (unsigned int)is_term(a1, "back_demodulant", 0LL) )
{
*(_DWORD *)v1 = 25;
return v1;
}
if ( (unsigned int)is_term(a1, "subsumer", 0LL) )
{
*(_DWORD *)v1 = 26;
return v1;
}
if ( !(unsigned int)is_term(a1, "<", 2LL)
&& !(unsigned int)is_term(a1, ">", 2LL)
&& !(unsigned int)is_term(a1, "<=", 2LL)
&& !(unsigned int)is_term(a1, ">=", 2LL)
&& !(unsigned int)is_term(a1, "=", 2LL) )
{
return 0LL;
}
v7 = *(_QWORD **)(a1 + 8);
v8 = *v7;
v9 = v7[1];
if ( (unsigned int)is_term(*v7, "weight", 0LL) )
{
*(_DWORD *)v1 = 27;
}
else if ( (unsigned int)is_term(v8, "variables", 0LL) )
{
*(_DWORD *)v1 = 28;
}
else if ( (unsigned int)is_term(v8, "depth", 0LL) )
{
*(_DWORD *)v1 = 29;
}
else if ( (unsigned int)is_term(v8, "literals", 0LL) )
{
*(_DWORD *)v1 = 30;
}
else
{
if ( !(unsigned int)is_term(v8, "level", 0LL) )
return 0LL;
*(_DWORD *)v1 = 31;
}
if ( (unsigned int)term_to_number(v9, v1 + 32) )
{
if ( (unsigned int)is_term(a1, "<", 2LL) )
{
*(_DWORD *)(v1 + 24) = 2;
}
else if ( (unsigned int)is_term(a1, ">", 2LL) )
{
*(_DWORD *)(v1 + 24) = 3;
}
else if ( (unsigned int)is_term(a1, "<=", 2LL) )
{
*(_DWORD *)(v1 + 24) = 4;
}
else if ( (unsigned int)is_term(a1, ">=", 2LL) )
{
*(_DWORD *)(v1 + 24) = 5;
}
else if ( (unsigned int)is_term(a1, "=", 2LL) )
{
*(_DWORD *)(v1 + 24) = 1;
}
return v1;
}
return 0LL;
}

canonical_decompiled_code:
__int64 __fastcall func3(__int64 a1)
{
__int64 v1; // r12
__int64 v2; // rax
__int64 v3; // rax
_QWORD *v5; // rax
__int64 v6; // rax
_QWORD *v7; // rax
__int64 v8; // r13
__int64 v9; // r14

v1 = func1();
if ( (unsigned int)is_term(a1, asc_8F4, 2LL) )
{
*(_DWORD *)v1 = 0;
LABEL_3:
v2 = func3(**(_QWORD **)(a1 + 8));
*(_QWORD *)(v1 + 8) = v2;
if ( v2 )
{
v3 = func3(*(_QWORD *)(*(_QWORD *)(a1 + 8) + 8LL));
*(_QWORD *)(v1 + 16) = v3;
if ( v3 )
return v1;
}
return 0LL;
}
if ( (unsigned int)is_term(a1, &asc_8F4[1], 2LL) )
{
*(_DWORD *)v1 = 1;
goto LABEL_3;
}
if ( (unsigned int)is_term(a1, &asc_8F4[2], 1LL) )
{
v5 = *(_QWORD **)(a1 + 8);
*(_DWORD *)v1 = 2;
v6 = func3(*v5);
*(_QWORD *)(v1 + 8) = v6;
if ( !v6 )
return 0LL;
return v1;
}
if ( (unsigned int)is_term(a1, "all", 0LL) )
{
*(_DWORD *)v1 = 3;
return v1;
}
if ( (unsigned int)is_term(a1, "positive", 0LL) )
{
*(_DWORD *)v1 = 9;
return v1;
}
if ( (unsigned int)is_term(a1, "negative", 0LL) )
{
*(_DWORD *)v1 = 10;
return v1;
}
if ( (unsigned int)is_term(a1, "mixed", 0LL) )
{
*(_DWORD *)v1 = 11;
return v1;
}
if ( (unsigned int)is_term(a1, "true", 0LL) )
{
*(_DWORD *)v1 = 13;
return v1;
}
if ( (unsigned int)is_term(a1, "false", 0LL) )
{
*(_DWORD *)v1 = 14;
return v1;
}
if ( (unsigned int)is_term(a1, "has_equality", 0LL) )
{
*(_DWORD *)v1 = 15;
return v1;
}
if ( (unsigned int)is_term(a1, "horn", 0LL) )
{
*(_DWORD *)v1 = 16;
return v1;
}
if ( (unsigned int)is_term(a1, "definite", 0LL) )
{
*(_DWORD *)v1 = 17;
return v1;
}
if ( (unsigned int)is_term(a1, "unit", 0LL) )
{
*(_DWORD *)v1 = 18;
return v1;
}
if ( (unsigned int)is_term(a1, "hint", 0LL) )
{
*(_DWORD *)v1 = 12;
return v1;
}
if ( (unsigned int)is_term(a1, "initial", 0LL) )
{
*(_DWORD *)v1 = 19;
return v1;
}
if ( (unsigned int)is_term(a1, "resolvent", 0LL) )
{
*(_DWORD *)v1 = 20;
return v1;
}
if ( (unsigned int)is_term(a1, "hyper_resolvent", 0LL) )
{
*(_DWORD *)v1 = 22;
return v1;
}
if ( (unsigned int)is_term(a1, "ur_resolvent", 0LL) )
{
*(_DWORD *)v1 = 21;
return v1;
}
if ( (unsigned int)is_term(a1, "factor", 0LL) )
{
*(_DWORD *)v1 = 23;
return v1;
}
if ( (unsigned int)is_term(a1, "paramodulant", 0LL) )
{
*(_DWORD *)v1 = 24;
return v1;
}
if ( (unsigned int)is_term(a1, "back_demodulant", 0LL) )
{
*(_DWORD *)v1 = 25;
return v1;
}
if ( (unsigned int)is_term(a1, "subsumer", 0LL) )
{
*(_DWORD *)v1 = 26;
return v1;
}
if ( !(unsigned int)is_term(a1, "<", 2LL)
&& !(unsigned int)is_term(a1, ">", 2LL)
&& !(unsigned int)is_term(a1, "<=", 2LL)
&& !(unsigned int)is_term(a1, ">=", 2LL)
&& !(unsigned int)is_term(a1, "=", 2LL) )
{
return 0LL;
}
v7 = *(_QWORD **)(a1 + 8);
v8 = *v7;
v9 = v7[1];
if ( (unsigned int)is_term(*v7, "weight", 0LL) )
{
*(_DWORD *)v1 = 27;
}
else if ( (unsigned int)is_term(v8, "variables", 0LL) )
{
*(_DWORD *)v1 = 28;
}
else if ( (unsigned int)is_term(v8, "depth", 0LL) )
{
*(_DWORD *)v1 = 29;
}
else if ( (unsigned int)is_term(v8, "literals", 0LL) )
{
*(_DWORD *)v1 = 30;
}
else
{
if ( !(unsigned int)is_term(v8, "level", 0LL) )
return 0LL;
*(_DWORD *)v1 = 31;
}
if ( (unsigned int)term_to_number(v9, v1 + 32) )
{
if ( (unsigned int)is_term(a1, "<", 2LL) )
{
*(_DWORD *)(v1 + 24) = 2;
}
else if ( (unsigned int)is_term(a1, ">", 2LL) )
{
*(_DWORD *)(v1 + 24) = 3;
}
else if ( (unsigned int)is_term(a1, "<=", 2LL) )
{
*(_DWORD *)(v1 + 24) = 4;
}
else if ( (unsigned int)is_term(a1, ">=", 2LL) )
{
*(_DWORD *)(v1 + 24) = 5;
}
else if ( (unsigned int)is_term(a1, "=", 2LL) )
{
*(_DWORD *)(v1 + 24) = 1;
}
return v1;
}
return 0LL;
}

original_code:
Clause_eval compile_clause_eval_rule(Term t)
{
  Clause_eval p = get_clause_eval();
  if (is_term(t, "&", 2)) {
    p->type = CL_EVAL_AND;
    p->left = compile_clause_eval_rule(((t)->args[0]));
    if (p->left == ((void *)0))
      return ((void *)0);
    p->right = compile_clause_eval_rule(((t)->args[1]));
    if (p->right == ((void *)0))
      return ((void *)0);
  }
  else if (is_term(t, "|", 2)) {
    p->type = CL_EVAL_OR;
    p->left = compile_clause_eval_rule(((t)->args[0]));
    if (p->left == ((void *)0))
      return ((void *)0);
    p->right = compile_clause_eval_rule(((t)->args[1]));
    if (p->right == ((void *)0))
      return ((void *)0);
  }
  else if (is_term(t, "-", 1)) {
    p->type = CL_EVAL_NOT;
    p->left = compile_clause_eval_rule(((t)->args[0]));
    if (p->left == ((void *)0))
      return ((void *)0);
  }
  else if (is_term(t, "all", 0))
    p->type = CL_EVAL_ALL;
  else if (is_term(t, "positive", 0))
    p->type = CL_EVAL_POSITIVE;
  else if (is_term(t, "negative", 0))
    p->type = CL_EVAL_NEGATIVE;
  else if (is_term(t, "mixed", 0))
    p->type = CL_EVAL_MIXED;
  else if (is_term(t, "true", 0))
    p->type = CL_EVAL_TRUE;
  else if (is_term(t, "false", 0))
    p->type = CL_EVAL_FALSE;
  else if (is_term(t, "has_equality", 0))
    p->type = CL_EVAL_HAS_EQUALITY;
  else if (is_term(t, "horn", 0))
    p->type = CL_EVAL_HORN;
  else if (is_term(t, "definite", 0))
    p->type = CL_EVAL_DEFINITE;
  else if (is_term(t, "unit", 0))
    p->type = CL_EVAL_UNIT;
  else if (is_term(t, "hint", 0))
    p->type = CL_EVAL_HINT;
  else if (is_term(t, "initial", 0))
    p->type = CL_EVAL_INITIAL;
  else if (is_term(t, "resolvent", 0))
    p->type = CL_EVAL_RESOLVENT;
  else if (is_term(t, "hyper_resolvent", 0))
    p->type = CL_EVAL_HYPER_RESOLVENT;
  else if (is_term(t, "ur_resolvent", 0))
    p->type = CL_EVAL_UR_RESOLVENT;
  else if (is_term(t, "factor", 0))
    p->type = CL_EVAL_FACTOR;
  else if (is_term(t, "paramodulant", 0))
    p->type = CL_EVAL_PARAMODULANT;
  else if (is_term(t, "back_demodulant", 0))
    p->type = CL_EVAL_BACK_DEMODULANT;
  else if (is_term(t, "subsumer", 0))
    p->type = CL_EVAL_SUBSUMER;
  else if (is_term(t, "<", 2) ||
    is_term(t, ">", 2) ||
    is_term(t, "<=", 2) ||
    is_term(t, ">=", 2) ||
    is_term(t, "=", 2)) {
    Term a0 = ((t)->args[0]);
    Term a1 = ((t)->args[1]);
    if (is_term(a0, "weight", 0))
      p->type = CL_EVAL_WEIGHT;
    else if (is_term(a0, "variables", 0))
      p->type = CL_EVAL_VARIABLES;
    else if (is_term(a0, "depth", 0))
      p->type = CL_EVAL_DEPTH;
    else if (is_term(a0, "literals", 0))
      p->type = CL_EVAL_LITERALS;
    else if (is_term(a0, "level", 0))
      p->type = CL_EVAL_LEVEL;
    else
      return ((void *)0);
    if (!term_to_number(a1, &(p->test_val)))
      return ((void *)0);
    if (is_term(t, "<", 2))
      p->relation = LESS_THAN;
    else if (is_term(t, ">", 2))
      p->relation = GREATER_THAN;
    else if (is_term(t, "<=", 2))
      p->relation = LESS_THAN_OR_SAME_AS;
    else if (is_term(t, ">=", 2))
      p->relation = GREATER_THAN_OR_SAME_AS;
    else if (is_term(t, "=", 2))
      p->relation = SAME_AS;
  }
  else
    return ((void *)0);
  return p;
}

canonical_original_code:
struct clause_eval *compile_clause_eval_rule(struct term *t)
{
  struct clause_eval *p = get_clause_eval();
  if (is_term(t, "&", 2)) {
    p->type = CL_EVAL_AND;
    p->left = compile_clause_eval_rule(((t)->args[0]));
    if (p->left == ((void *)0))
      return ((void *)0);
    p->right = compile_clause_eval_rule(((t)->args[1]));
    if (p->right == ((void *)0))
      return ((void *)0);
  }
  else if (is_term(t, "|", 2)) {
    p->type = CL_EVAL_OR;
    p->left = compile_clause_eval_rule(((t)->args[0]));
    if (p->left == ((void *)0))
      return ((void *)0);
    p->right = compile_clause_eval_rule(((t)->args[1]));
    if (p->right == ((void *)0))
      return ((void *)0);
  }
  else if (is_term(t, "-", 1)) {
    p->type = CL_EVAL_NOT;
    p->left = compile_clause_eval_rule(((t)->args[0]));
    if (p->left == ((void *)0))
      return ((void *)0);
  }
  else if (is_term(t, "all", 0))
    p->type = CL_EVAL_ALL;
  else if (is_term(t, "positive", 0))
    p->type = CL_EVAL_POSITIVE;
  else if (is_term(t, "negative", 0))
    p->type = CL_EVAL_NEGATIVE;
  else if (is_term(t, "mixed", 0))
    p->type = CL_EVAL_MIXED;
  else if (is_term(t, "true", 0))
    p->type = CL_EVAL_TRUE;
  else if (is_term(t, "false", 0))
    p->type = CL_EVAL_FALSE;
  else if (is_term(t, "has_equality", 0))
    p->type = CL_EVAL_HAS_EQUALITY;
  else if (is_term(t, "horn", 0))
    p->type = CL_EVAL_HORN;
  else if (is_term(t, "definite", 0))
    p->type = CL_EVAL_DEFINITE;
  else if (is_term(t, "unit", 0))
    p->type = CL_EVAL_UNIT;
  else if (is_term(t, "hint", 0))
    p->type = CL_EVAL_HINT;
  else if (is_term(t, "initial", 0))
    p->type = CL_EVAL_INITIAL;
  else if (is_term(t, "resolvent", 0))
    p->type = CL_EVAL_RESOLVENT;
  else if (is_term(t, "hyper_resolvent", 0))
    p->type = CL_EVAL_HYPER_RESOLVENT;
  else if (is_term(t, "ur_resolvent", 0))
    p->type = CL_EVAL_UR_RESOLVENT;
  else if (is_term(t, "factor", 0))
    p->type = CL_EVAL_FACTOR;
  else if (is_term(t, "paramodulant", 0))
    p->type = CL_EVAL_PARAMODULANT;
  else if (is_term(t, "back_demodulant", 0))
    p->type = CL_EVAL_BACK_DEMODULANT;
  else if (is_term(t, "subsumer", 0))
    p->type = CL_EVAL_SUBSUMER;
  else if (is_term(t, "<", 2) ||
    is_term(t, ">", 2) ||
    is_term(t, "<=", 2) ||
    is_term(t, ">=", 2) ||
    is_term(t, "=", 2)) {
    struct term *a0 = ((t)->args[0]);
    struct term *a1 = ((t)->args[1]);
    if (is_term(a0, "weight", 0))
      p->type = CL_EVAL_WEIGHT;
    else if (is_term(a0, "variables", 0))
      p->type = CL_EVAL_VARIABLES;
    else if (is_term(a0, "depth", 0))
      p->type = CL_EVAL_DEPTH;
    else if (is_term(a0, "literals", 0))
      p->type = CL_EVAL_LITERALS;
    else if (is_term(a0, "level", 0))
      p->type = CL_EVAL_LEVEL;
    else
      return ((void *)0);
    if (!term_to_number(a1, &(p->test_val)))
      return ((void *)0);
    if (is_term(t, "<", 2))
      p->relation = LESS_THAN;
    else if (is_term(t, ">", 2))
      p->relation = GREATER_THAN;
    else if (is_term(t, "<=", 2))
      p->relation = LESS_THAN_OR_SAME_AS;
    else if (is_term(t, ">=", 2))
      p->relation = GREATER_THAN_OR_SAME_AS;
    else if (is_term(t, "=", 2))
      p->relation = SAME_AS;
  }
  else
    return ((void *)0);
  return p;
}


decompiled_code:
__int64 __fastcall rule_contains_semantics(__int64 a1)
{
__int64 result; // rax
int v2; // er8

if ( *(_DWORD *)a1 > 1u )
return (unsigned int)(*(_DWORD *)a1 - 13) <= 1;
v2 = rule_contains_semantics(*(_QWORD *)(a1 + 8));
result = 1LL;
if ( !v2 )
result = (unsigned int)rule_contains_semantics(*(_QWORD *)(a1 + 16)) != 0;
return result;
}

canonical_decompiled_code:
__int64 __fastcall func5(__int64 a1)
{
__int64 result; // rax
int v2; // er8

if ( *(_DWORD *)a1 > 1u )
return (unsigned int)(*(_DWORD *)a1 - 13) <= 1;
v2 = func5(*(_QWORD *)(a1 + 8));
result = 1LL;
if ( !v2 )
result = (unsigned int)func5(*(_QWORD *)(a1 + 16)) != 0;
return result;
}

original_code:
BOOL rule_contains_semantics(Clause_eval p)
{
  if (p->type == CL_EVAL_AND || p->type == CL_EVAL_OR) {
    return (rule_contains_semantics(p->left) ||
     rule_contains_semantics(p->right));
  }
  else if (p->type == CL_EVAL_OR)
    return rule_contains_semantics(p->left);
  else
    return p->type == CL_EVAL_TRUE || p->type == CL_EVAL_FALSE;
}

canonical_original_code:
enum BOOL rule_contains_semantics(struct clause_eval *p)
{
  if (p->type == CL_EVAL_AND || p->type == CL_EVAL_OR) {
    return (rule_contains_semantics(p->left) ||
     rule_contains_semantics(p->right));
  }
  else if (p->type == CL_EVAL_OR)
    return rule_contains_semantics(p->left);
  else
    return p->type == CL_EVAL_TRUE || p->type == CL_EVAL_FALSE;
}


decompiled_code:
__int64 __fastcall sum_indexes(__int64 a1)
{
int v1; // eax
_DWORD **v2; // rdx
__int64 v3; // rcx
unsigned int v4; // er8
_DWORD **v5; // rax
__int64 v6; // rcx

v1 = *(unsigned __int8 *)(a1 + 4);
if ( !(_BYTE)v1 )
return (unsigned int)-1;
v2 = *(_DWORD ***)(a1 + 8);
v3 = (unsigned int)(v1 - 1);
v4 = 0;
v5 = v2 + 1;
v6 = (__int64)&v2[v3 + 1];
while ( 1 )
{
v4 += **v2;
v2 = v5;
if ( v5 == (_DWORD **)v6 )
break;
++v5;
}
return v4;
}

canonical_decompiled_code:
__int64 __fastcall func0(__int64 a1)
{
int v1; // eax
_DWORD **v2; // rdx
__int64 v3; // rcx
unsigned int v4; // er8
_DWORD **v5; // rax
__int64 v6; // rcx

v1 = *(unsigned __int8 *)(a1 + 4);
if ( !(_BYTE)v1 )
return (unsigned int)-1;
v2 = *(_DWORD ***)(a1 + 8);
v3 = (unsigned int)(v1 - 1);
v4 = 0;
v5 = v2 + 1;
v6 = (__int64)&v2[v3 + 1];
while ( 1 )
{
v4 += **v2;
v2 = v5;
if ( v5 == (_DWORD **)v6 )
break;
++v5;
}
return v4;
}

original_code:
static
int sum_indexes(Term t)
{
  if (((t)->arity) == 0)
    return -1;
  else {
    int sum = 0;
    int i;
    for (i = 0; i < ((t)->arity); i++)
      sum += ((((t)->args[i]))->private_symbol);
    return sum;
  }
}

canonical_original_code:
static int sum_indexes(struct term *t)
{
  if (((t)->arity) == 0)
    return -1;
  else {
    int sum = 0;
    int i;
    for (i = 0; i < ((t)->arity); i++)
      sum += ((((t)->args[i]))->private_symbol);
    return sum;
  }
}

variable_types: sum int


decompiled_code:
__int64 __fastcall compare_cells(__int64 a1, __int64 a2)
{
__int64 v2; // rcx
__int64 v3; // rdx
int v4; // eax
int v5; // er8
int v6; // er10
__int64 result; // rax
int v8; // edx
int v9; // er8
int v10; // er9

v2 = *(_QWORD *)(a1 + 48);
v3 = *(_QWORD *)(a2 + 48);
v4 = *(_DWORD *)(v2 + 20);
v5 = *(_DWORD *)(v3 + 20);
if ( v4 == 1 )
{
result = 3LL;
if ( v5 != 1 )
return result;
}
else
{
if ( v5 == 1 )
return 2LL;
if ( Skolems_last )
{
if ( v4 == 2 )
{
result = 3LL;
if ( v5 != 2 )
return result;
}
else
{
result = 2LL;
if ( v5 == 2 )
return result;
}
}
}
v6 = *(_DWORD *)(a2 + 40);
result = 2LL;
if ( *(_DWORD *)(a1 + 40) >= v6 )
{
result = 3LL;
if ( *(_DWORD *)(a1 + 40) <= v6 )
{
v8 = *(_DWORD *)(v3 + 4);
result = 2LL;
if ( *(_DWORD *)(v2 + 4) >= v8 )
{
result = 3LL;
if ( *(_DWORD *)(v2 + 4) <= v8 )
{
sum_indexes(*(_QWORD *)(a1 + 8));
v9 = sum_indexes(*(_QWORD *)(a2 + 8));
result = 2LL;
if ( v10 >= v9 )
result = 2 * (unsigned int)(v10 > v9) + 1;
}
}
}
}
return result;
}

canonical_decompiled_code:
__int64 __fastcall func1(__int64 a1, __int64 a2)
{
__int64 v2; // rcx
__int64 v3; // rdx
int v4; // eax
int v5; // er8
int v6; // er10
__int64 result; // rax
int v8; // edx
int v9; // er8
int v10; // er9

v2 = *(_QWORD *)(a1 + 48);
v3 = *(_QWORD *)(a2 + 48);
v4 = *(_DWORD *)(v2 + 20);
v5 = *(_DWORD *)(v3 + 20);
if ( v4 == 1 )
{
result = 3LL;
if ( v5 != 1 )
return result;
}
else
{
if ( v5 == 1 )
return 2LL;
if ( Skolems_last )
{
if ( v4 == 2 )
{
result = 3LL;
if ( v5 != 2 )
return result;
}
else
{
result = 2LL;
if ( v5 == 2 )
return result;
}
}
}
v6 = *(_DWORD *)(a2 + 40);
result = 2LL;
if ( *(_DWORD *)(a1 + 40) >= v6 )
{
result = 3LL;
if ( *(_DWORD *)(a1 + 40) <= v6 )
{
v8 = *(_DWORD *)(v3 + 4);
result = 2LL;
if ( *(_DWORD *)(v2 + 4) >= v8 )
{
result = 3LL;
if ( *(_DWORD *)(v2 + 4) <= v8 )
{
func0(*(_QWORD *)(a1 + 8));
v9 = func0(*(_QWORD *)(a2 + 8));
result = 2LL;
if ( v10 >= v9 )
result = 2 * (unsigned int)(v10 > v9) + 1;
}
}
}
}
return result;
}

original_code:
static
Ordertype compare_cells(struct cell *a, struct cell *b)
{
  if (a->symbol->attribute == EQUALITY_SYMBOL &&
      b->symbol->attribute != EQUALITY_SYMBOL) return GREATER_THAN;
  else if (a->symbol->attribute != EQUALITY_SYMBOL &&
    b->symbol->attribute == EQUALITY_SYMBOL) return LESS_THAN;
  else if (Skolems_last &&
    a->symbol->attribute == SKOLEM_SYMBOL &&
    b->symbol->attribute != SKOLEM_SYMBOL) return GREATER_THAN;
  else if (Skolems_last &&
    a->symbol->attribute != SKOLEM_SYMBOL &&
    b->symbol->attribute == SKOLEM_SYMBOL) return LESS_THAN;
  else if (a->max_index < b->max_index) return LESS_THAN;
  else if (a->max_index > b->max_index) return GREATER_THAN;
  else if (a->symbol->mace_sn < b->symbol->mace_sn) return LESS_THAN;
  else if (a->symbol->mace_sn > b->symbol->mace_sn) return GREATER_THAN;
  else if (sum_indexes(a->eterm) <
           sum_indexes(b->eterm)) return LESS_THAN;
  else if (sum_indexes(a->eterm) >
           sum_indexes(b->eterm)) return GREATER_THAN;
  else
    return SAME_AS;
}

canonical_original_code:
static enum Ordertype compare_cells(struct cell *a, struct cell *b)
{
  if (a->symbol->attribute == EQUALITY_SYMBOL &&
      b->symbol->attribute != EQUALITY_SYMBOL) return GREATER_THAN;
  else if (a->symbol->attribute != EQUALITY_SYMBOL &&
    b->symbol->attribute == EQUALITY_SYMBOL) return LESS_THAN;
  else if (Skolems_last &&
    a->symbol->attribute == SKOLEM_SYMBOL &&
    b->symbol->attribute != SKOLEM_SYMBOL) return GREATER_THAN;
  else if (Skolems_last &&
    a->symbol->attribute != SKOLEM_SYMBOL &&
    b->symbol->attribute == SKOLEM_SYMBOL) return LESS_THAN;
  else if (a->max_index < b->max_index) return LESS_THAN;
  else if (a->max_index > b->max_index) return GREATER_THAN;
  else if (a->symbol->mace_sn < b->symbol->mace_sn) return LESS_THAN;
  else if (a->symbol->mace_sn > b->symbol->mace_sn) return GREATER_THAN;
  else if (sum_indexes(a->eterm) <
           sum_indexes(b->eterm)) return LESS_THAN;
  else if (sum_indexes(a->eterm) >
           sum_indexes(b->eterm)) return GREATER_THAN;
  else
    return SAME_AS;
}

variable_types: struct cell { int id; struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *eterm; struct term *value; struct term *occurrences; struct term **possible; int max_index; struct symbol_data { int sn; int mace_sn; int arity; int type; int base; int attribute; struct symbol_data *next; } *symbol; } *

variable_types:
b
struct cell *

user_defined_types: struct cell { int id; struct term *eterm; struct term *value; struct term *occurrences; struct term **possible; int max_index; struct symbol_data *symbol; }


decompiled_code:
int __fastcall order_cells(int a1)
{
unsigned int v2; // er8
__int64 v3; // rdi
__int64 v4; // rax
__int64 v5; // rsi
__int64 v6; // rdx
__int64 v7; // rcx
__int64 v8; // rdx
int result; // eax
__int64 v10; // rbx
_DWORD *v11; // rbp

v2 = Number_of_cells;
v3 = Ordered_cells;
if ( Number_of_cells > 0 )
{
v4 = Ordered_cells;
v5 = Ordered_cells + 8LL * (unsigned int)(Number_of_cells - 1) + 8;
v6 = 0LL;
do
{
v4 += 8LL;
v7 = v6 + Cells;
v6 += 56LL;
*(_QWORD *)(v4 - 8) = v7;
}
while ( v5 != v4 );
}
merge_sort(v3, v2, compare_cells);
if ( !Skolems_last )
{
result = Number_of_cells;
goto LABEL_17;
}
if ( Number_of_cells <= 0 )
{
result = 0;
LABEL_17:
First_skolem_cell = result;
if ( !a1 )
return result;
goto LABEL_10;
}
v8 = Ordered_cells;
result = 0;
while ( *(_DWORD *)(*(_QWORD *)(*(_QWORD *)v8 + 48LL) + 20LL) != 2 )
{
++result;
v8 += 8LL;
if ( result == Number_of_cells )
goto LABEL_17;
}
First_skolem_cell = result;
if ( a1 )
{
LABEL_10:
v10 = 0LL;
printf("\n%% Cell selection order:\n\n");
if ( Number_of_cells > 0 )
{
do
{
while ( 1 )
{
v11 = *(_DWORD **)(*(_QWORD *)(Ordered_cells + 8 * v10) + 8LL);
if ( !(unsigned int)is_eq_symbol((unsigned int)-*v11) )
break;
if ( Number_of_cells <= (int)++v10 )
goto LABEL_15;
}
++v10;
fwrite_term_nl(stdout, v11);
}
while ( Number_of_cells > (int)v10 );
}
LABEL_15:
result = fflush(stdout);
}
return result;
}

canonical_decompiled_code:
int __fastcall func2(int a1)
{
unsigned int v2; // er8
__int64 v3; // rdi
__int64 v4; // rax
__int64 v5; // rsi
__int64 v6; // rdx
__int64 v7; // rcx
__int64 v8; // rdx
int result; // eax
__int64 v10; // rbx
_DWORD *v11; // rbp

v2 = Number_of_cells;
v3 = Ordered_cells;
if ( Number_of_cells > 0 )
{
v4 = Ordered_cells;
v5 = Ordered_cells + 8LL * (unsigned int)(Number_of_cells - 1) + 8;
v6 = 0LL;
do
{
v4 += 8LL;
v7 = v6 + Cells;
v6 += 56LL;
*(_QWORD *)(v4 - 8) = v7;
}
while ( v5 != v4 );
}
merge_sort(v3, v2, compare_cells);
if ( !Skolems_last )
{
result = Number_of_cells;
goto LABEL_17;
}
if ( Number_of_cells <= 0 )
{
result = 0;
LABEL_17:
First_skolem_cell = result;
if ( !a1 )
return result;
goto LABEL_10;
}
v8 = Ordered_cells;
result = 0;
while ( *(_DWORD *)(*(_QWORD *)(*(_QWORD *)v8 + 48LL) + 20LL) != 2 )
{
++result;
v8 += 8LL;
if ( result == Number_of_cells )
goto LABEL_17;
}
First_skolem_cell = result;
if ( a1 )
{
LABEL_10:
v10 = 0LL;
printf("\n%% Cell selection order:\n\n");
if ( Number_of_cells > 0 )
{
do
{
while ( 1 )
{
v11 = *(_DWORD **)(*(_QWORD *)(Ordered_cells + 8 * v10) + 8LL);
if ( !(unsigned int)is_eq_symbol((unsigned int)-*v11) )
break;
if ( Number_of_cells <= (int)++v10 )
goto LABEL_15;
}
++v10;
fwrite_term_nl(stdout, v11);
}
while ( Number_of_cells > (int)v10 );
}
LABEL_15:
result = fflush(stdout);
}
return result;
}

original_code:
void order_cells(BOOL verbose)
{
  int i;
  for (i = 0; i < Number_of_cells; i++)
    Ordered_cells[i] = Cells + i;
  merge_sort((void **) Ordered_cells, Number_of_cells,
             (Ordertype (*) (void*,void*)) compare_cells);
  if (Skolems_last) {
    for (i = 0; i < Number_of_cells; i++)
      if (Ordered_cells[i]->symbol->attribute == SKOLEM_SYMBOL)
 break;
    First_skolem_cell = i;
  }
  else
    First_skolem_cell = Number_of_cells;
  if (verbose) {
    printf("\n%% Cell selection order:\n\n");
    for (i = 0; i < Number_of_cells; i++) {
      Term t = Ordered_cells[i]->eterm;
      if (!is_eq_symbol((-((t)->private_symbol))))
 fwrite_term_nl(stdout, t);
    }
    fflush(stdout);
  }
}

canonical_original_code:
void order_cells(enum BOOL verbose)
{
  int i;
  for (i = 0; i < Number_of_cells; i++)
    Ordered_cells[i] = Cells + i;
  merge_sort((void **) Ordered_cells, Number_of_cells,
             (enum Ordertype (*)(void *, void *)) compare_cells);
  if (Skolems_last) {
    for (i = 0; i < Number_of_cells; i++)
      if (Ordered_cells[i]->symbol->attribute == SKOLEM_SYMBOL)
 break;
    First_skolem_cell = i;
  }
  else
    First_skolem_cell = Number_of_cells;
  if (verbose) {
    printf("\n%% Cell selection order:\n\n");
    for (i = 0; i < Number_of_cells; i++) {
      struct term *t = Ordered_cells[i]->eterm;
      if (!is_eq_symbol((-((t)->private_symbol))))
 fwrite_term_nl(stdout, t);
    }
    fflush(stdout);
  }
}

variable_types:
verbose
enum BOOL { FALSE=0, TRUE=1 }


decompiled_code:
__int64 done_with_hints()
{
__int64 result; // rax

if ( !(unsigned int)lindex_empty(Hints_idx) || !(unsigned int)clist_empty(Redundant_hints) )
puts("ERROR: Hints index not empty!");
lindex_destroy(Hints_idx);
if ( Back_demod_hints )
mindex_destroy(Back_demod_idx);
Hints_idx = 0LL;
result = clist_free(Redundant_hints);
Redundant_hints = 0LL;
return result;
}

canonical_decompiled_code:
__int64 func3()
{
__int64 result; // rax

if ( !(unsigned int)lindex_empty(Hints_idx) || !(unsigned int)clist_empty(Redundant_hints) )
puts("ERROR: Hints index not empty!");
lindex_destroy(Hints_idx);
if ( Back_demod_hints )
mindex_destroy(Back_demod_idx);
Hints_idx = 0LL;
result = clist_free(Redundant_hints);
Redundant_hints = 0LL;
return result;
}

original_code:
void done_with_hints(void)
{
  if (!lindex_empty(Hints_idx) ||
      !clist_empty(Redundant_hints))
    printf("ERROR: Hints index not empty!\n");
  lindex_destroy(Hints_idx);
  if (Back_demod_hints)
    mindex_destroy(Back_demod_idx);
  Hints_idx = ((void *)0);
  clist_free(Redundant_hints);
  Redundant_hints = ((void *)0);
}

canonical_original_code:
void done_with_hints()
{
  if (!lindex_empty(Hints_idx) ||
      !clist_empty(Redundant_hints))
    printf("ERROR: Hints index not empty!\n");
  lindex_destroy(Hints_idx);
  if (Back_demod_hints)
    mindex_destroy(Back_demod_idx);
  Hints_idx = ((void *)0);
  clist_free(Redundant_hints);
  Redundant_hints = ((void *)0);
}


decompiled_code:
__int64 redundant_hints()
{
return clist_length(Redundant_hints);
}

canonical_decompiled_code:
__int64 func4()
{
return clist_length(Redundant_hints);
}

original_code:
int redundant_hints(void)
{
  return clist_length(Redundant_hints);
}

canonical_original_code:
int redundant_hints()
{
  return clist_length(Redundant_hints);
}


decompiled_code:
__int64 __fastcall input_clauses(_QWORD *a1)
{
__int64 v1; // r12
__int64 result; // rax

if ( !a1 )
return 0LL;
v1 = input_clauses(a1[1]);
if ( (unsigned int)has_input_just(*a1) )
result = plist_prepend(v1, *a1);
else
result = v1;
return result;
}

canonical_decompiled_code:
__int64 __fastcall func3(_QWORD *a1)
{
__int64 v1; // r12
__int64 result; // rax

if ( !a1 )
return 0LL;
v1 = func3(a1[1]);
if ( (unsigned int)has_input_just(*a1) )
result = plist_prepend(v1, *a1);
else
result = v1;
return result;
}

original_code:
Plist input_clauses(Plist a)
{
  if (a == ((void *)0))
    return ((void *)0);
  else {
    Plist c = input_clauses(a->next);
    if (has_input_just(a->v))
      return plist_prepend(c, a->v);
    else
      return c;
  }
}

canonical_original_code:
struct plist *input_clauses(struct plist *a)
{
  if (a == ((void *)0))
    return ((void *)0);
  else {
    struct plist *c = input_clauses(a->next);
    if (has_input_just(a->v))
      return plist_prepend(c, a->v);
    else
      return c;
  }
}

variable_types:
a
struct plist *

variable_types: struct plist { void *v; struct plist *next; } *


decompiled_code:
__int64 __fastcall delete_clauses(__int64 *a1)
{
__int64 result; // rax

if ( a1 )
{
delete_clauses(a1[1]);
delete_clause(*a1);
result = free_plist(a1);
}
return result;
}

canonical_decompiled_code:
__int64 __fastcall func7(__int64 *a1)
{
__int64 result; // rax

if ( a1 )
{
func7(a1[1]);
func4(*a1);
result = free_plist(a1);
}
return result;
}

original_code:
void delete_clauses(Plist p)
{
  if (p != ((void *)0)) {
    delete_clauses(p->next);
    delete_clause(p->v);
    free_plist(p);
  }
}

canonical_original_code:
void delete_clauses(struct plist *p)
{
  if (p != ((void *)0)) {
    delete_clauses(p->next);
    delete_clause(p->v);
    free_plist(p);
  }
}


decompiled_code:
__int64 __fastcall ptr_compare(unsigned __int64 a1, unsigned __int64 a2)
{
__int64 result; // rax

result = 2LL;
if ( a1 >= a2 )
result = 2 * (unsigned int)(a1 > a2) + 1;
return result;
}

canonical_decompiled_code:
__int64 __fastcall func0(unsigned __int64 a1, unsigned __int64 a2)
{
__int64 result; // rax

result = 2LL;
if ( a1 >= a2 )
result = 2 * (unsigned int)(a1 > a2) + 1;
return result;
}

original_code:
static Ordertype ptr_compare(void *i1, void *i2)
{
  return (i1 < i2 ? LESS_THAN : (i1 > i2 ? GREATER_THAN : SAME_AS));
}

canonical_original_code:
static enum Ordertype ptr_compare(void *i1, void *i2)
{
  return (i1 < i2 ? LESS_THAN : (i1 > i2 ? GREATER_THAN : SAME_AS));
}


main

decompiled_code:
int __cdecl __noreturn main(int argc, const char **argv, const char **envp)
{
double v3; // xmm0_8
int v4; // er12
int v5; // eax
int *v6; // rbp
int *v7; // r15
__int64 v8; // r14
int v9; // eax
int v10; // ebx
__int64 v11; // rax
__int64 v12; // rax
__int64 v13; // rbx
__int64 v14; // rax
__int64 v15; // rsi
int v16; // er13
unsigned int v17; // ebx
double v18; // xmm0_8
__int64 v19; // r12
int v20; // eax
int v21; // ebx
double v22; // [rsp+8h] [rbp-40h]
double v23; // [rsp+8h] [rbp-40h]

if ( argc != 3 )
{
puts("need 2 args: size seed");
exit(0);
}
v4 = atoi(argv[1]);
v5 = atoi(argv[2]);
srand(v5);
v6 = (int *)malloc(4LL * v4);
random_permutation(v6, (unsigned int)v4);
puts("starting insert");
fflush(stdout);
if ( v4 <= 0 )
{
v8 = 0LL;
}
else
{
v7 = v6;
v8 = 0LL;
do
{
v9 = *v7++;
v10 = v9 + 1;
printf("inserting %4d\n", (unsigned int)(v9 + 1));
v8 = avl_insert(v8, v10, ptr_compare);
avl_check(v8, ptr_compare);
}
while ( v7 != &v6[v4 - 1 + 1] );
}
p_avl(v8, 0LL);
puts("finished insert");
fflush(stdout);
v11 = avl_smallest(v8);
printf("smallest item is %d.\n", v11);
v12 = avl_largest(v8);
printf("largest item is %d.\n", v12);
avl_position(v8, *v6 + 1LL, ptr_compare);
printf("position of %d is %.4f.\n", (unsigned int)(*v6 + 1), v3);
if ( v4 > 0 )
{
v13 = 1LL;
do
{
v22 = avl_position(v8, v13, ptr_compare);
v14 = avl_item_at_position(v8);
v15 = (unsigned int)v13++;
printf("item %d, position %.12f, item=%d.\n", v15, v22, v14);
}
while ( v4 >= (int)v13 );
}
v16 = 0;
do
{
v23 = (double)v16++ / 100.0;
v17 = avl_item_at_position(v8);
v18 = avl_position(v8, (int)v17, ptr_compare);
printf("Position %.2f, item %d, position=%.4f.\n", v23, v17, v18);
}
while ( v16 != 101 );
random_permutation(v6, (unsigned int)v4);
puts("starting delete");
fflush(stdout);
if ( v4 > 0 )
{
v19 = (__int64)&v6[v4 - 1 + 1];
do
{
v20 = *v6++;
v21 = v20 + 1;
printf("********************************** Removing %d\n", (unsigned int)(v20 + 1));
v8 = avl_delete(v8, v21, ptr_compare);
avl_check(v8, ptr_compare);
}
while ( (int *)v19 != v6 );
}
p_avl(v8, 0LL);
exit(0);
}

original_code:
int main(int argc, char **argv)
{
  struct mace_options opt;
  Plist clauses;
  Mace_results results;
  BOOL prover_compatability_mode = member_args(argc, argv, "-c");
  init_standard_ladr();
  init_mace_options(&opt);
  init_attrs();
  if (member_args(argc, argv, "help") ||
      member_args(argc, argv, "-help")) {
    usage_message(stderr, &opt);
    exit(1);
  }
  print_banner(argc, argv, "Mace4", "2009-11A", "November 2009", FALSE);
  set_program_name("Mace4");
  signal(2, mace4_sig_handler);
  signal(10, mace4_sig_handler);
  signal(11, mace4_sig_handler);
  clauses = read_mace4_input(argc, argv, prover_compatability_mode, &opt);
  print_separator(stdout, "CLAUSES FOR SEARCH", TRUE);
  fwrite_clause_list(stdout, clauses, "mace4_clauses", CL_FORM_BARE);
  print_separator(stdout, "end of clauses for search", TRUE);
  results = mace4(clauses, &opt);
  mace4_exit(results->return_code);
  exit(0);
}

canonical_original_code:
int main(int argc, char **argv)
{
  struct mace_options opt;
  struct plist *clauses;
  struct mace_results *results;
  enum BOOL prover_compatability_mode = member_args(argc, argv, "-c");
  init_standard_ladr();
  init_mace_options(&opt);
  init_attrs();
  if (member_args(argc, argv, "help") ||
      member_args(argc, argv, "-help")) {
    usage_message(stderr, &opt);
    exit(1);
  }
  print_banner(argc, argv, "Mace4", "2009-11A", "November 2009", FALSE);
  set_program_name("Mace4");
  signal(2, mace4_sig_handler);
  signal(10, mace4_sig_handler);
  signal(11, mace4_sig_handler);
  clauses = read_mace4_input(argc, argv, prover_compatability_mode, &opt);
  print_separator(stdout, "CLAUSES FOR SEARCH", TRUE);
  fwrite_clause_list(stdout, clauses, "mace4_clauses", CL_FORM_BARE);
  print_separator(stdout, "end of clauses for search", TRUE);
  results = mace4(clauses, &opt);
  mace4_exit(results->return_code);
  exit(0);
}

variable_types: argc int

variable_types:
argv
char **

variable_types: struct mace_options { int print_models; int domain_size; int iterate; }

variable_types: struct mace_results { enum BOOL { FALSE=0, TRUE=1 } success; struct plist { void *v; struct plist *next; } *models; double user_seconds; int return_code; } *


decompiled_code:
__int64 __fastcall uncompress_term(__int64 a1, int *a2)
{
__int64 v3; // rax
int v4; // edi
unsigned int v5; // eax
__int64 v6; // r12
__int64 v7; // rbx
_QWORD *v8; // r14

v3 = *a2;
*a2 = v3 + 1;
v4 = *(char *)(a1 + v3);
if ( (char)v4 <= 0 )
return get_variable_term((unsigned int)-v4);
v5 = sn_to_arity((unsigned int)(char)v4);
v6 = get_rigid_term_dangerously((unsigned int)(char)v4, v5);
if ( *(_BYTE *)(v6 + 4) )
{
v7 = 0LL;
do
{
v8 = (_QWORD *)(*(_QWORD *)(v6 + 8) + 8 * v7++);
*v8 = uncompress_term(a1, a2);
}
while ( *(unsigned __int8 *)(v6 + 4) > (int)v7 );
}
return v6;
}

canonical_decompiled_code:
__int64 __fastcall func1(__int64 a1, int *a2)
{
__int64 v3; // rax
int v4; // edi
unsigned int v5; // eax
__int64 v6; // r12
__int64 v7; // rbx
_QWORD *v8; // r14

v3 = *a2;
*a2 = v3 + 1;
v4 = *(char *)(a1 + v3);
if ( (char)v4 <= 0 )
return get_variable_term((unsigned int)-v4);
v5 = sn_to_arity((unsigned int)(char)v4);
v6 = get_rigid_term_dangerously((unsigned int)(char)v4, v5);
if ( *(_BYTE *)(v6 + 4) )
{
v7 = 0LL;
do
{
v8 = (_QWORD *)(*(_QWORD *)(v6 + 8) + 8 * v7++);
*v8 = func1(a1, a2);
}
while ( *(unsigned __int8 *)(v6 + 4) > (int)v7 );
}
return v6;
}

original_code:
Term uncompress_term(char *s, int *ip)
{
  char c = s[(*ip)++];
  if (c <= 0)
    return get_variable_term(-c);
  else {
    int arity = sn_to_arity(c);
    Term t = get_rigid_term_dangerously(c, arity);
    int i;
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = uncompress_term(s, ip);
    return t;
  }
}

canonical_original_code:
struct term *uncompress_term(char *s, int *ip)
{
  char c = s[(*ip)++];
  if (c <= 0)
    return get_variable_term(-c);
  else {
    int arity = sn_to_arity(c);
    struct term *t = get_rigid_term_dangerously(c, arity);
    int i;
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = uncompress_term(s, ip);
    return t;
  }
}

variable_types:
ip
int *

variable_types: i int


decompiled_code:
int p_mindex_mem()
{
return fprint_mindex_mem(stdout, 1);
}

canonical_decompiled_code:
int func10()
{
return func9(stdout, 1);
}

original_code:
void p_mindex_mem()
{
  fprint_mindex_mem(stdout, TRUE);
}


decompiled_code:
__int64 __fastcall intersect_clauses(__int64 *a1, _QWORD *a2)
{
__int64 v2; // r12

if ( !a1 )
return 0LL;
v2 = intersect_clauses(a1[1]);
if ( clause_member_plist(a2, *a1) )
return plist_prepend(v2, *a1);
return v2;
}

canonical_decompiled_code:
__int64 __fastcall func1(__int64 *a1, _QWORD *a2)
{
__int64 v2; // r12

if ( !a1 )
return 0LL;
v2 = func1(a1[1]);
if ( func0(a2, *a1) )
return plist_prepend(v2, *a1);
return v2;
}

original_code:
Plist intersect_clauses(Plist a, Plist b)
{
  if (a == ((void *)0))
    return ((void *)0);
  else {
    Plist c = intersect_clauses(a->next, b);
    if (clause_member_plist(b, a->v))
      return plist_prepend(c, a->v);
    else
      return c;
  }
}

canonical_original_code:
struct plist *intersect_clauses(struct plist *a, struct plist *b)
{
  if (a == ((void *)0))
    return ((void *)0);
  else {
    struct plist *c = intersect_clauses(a->next, b);
    if (clause_member_plist(b, a->v))
      return plist_prepend(c, a->v);
    else
      return c;
  }
}

variable_types:
b
struct plist *

return_type: struct plist { void *v; struct plist *next; } *


decompiled_code:
int p_lindex_mem()
{
return fprint_lindex_mem(stdout, 1);
}

canonical_decompiled_code:
int func3()
{
return func2(stdout, 1);
}

original_code:
void p_lindex_mem()
{
  fprint_lindex_mem(stdout, TRUE);
}


decompiled_code:
__int64 __fastcall subst_terms(__int64 a1, __int64 a2, __int64 a3, __int64 a4)
{
__int64 v7; // rbx
int v8; // edi
char v9; // al
_QWORD *v10; // rbp
__int64 v12; // rax
unsigned int v13; // eax
__int64 v14; // rbp

v7 = 0LL;
v8 = *(_DWORD *)a1;
v9 = *(_BYTE *)(a1 + 4);
if ( v8 >= 0 )
{
if ( !v9 )
return a1;
do
{
LABEL_3:
v10 = (_QWORD *)(*(_QWORD *)(a1 + 8) + 8 * v7++);
*v10 = subst_terms(*v10, a2, a3, a4);
}
while ( *(unsigned __int8 *)(a1 + 4) > (int)v7 );
return a1;
}
if ( v9 )
goto LABEL_3;
v12 = sn_to_str((unsigned int)-v8);
if ( (unsigned int)string_member_plist(v12, a4) )
return a1;
v13 = position_of_term_in_tlist(a1, a2);
if ( v13 == -1 )
return a1;
v14 = ith_in_plist(a3, v13);
zap_term(a1);
return copy_term(v14);
}

canonical_decompiled_code:
__int64 __fastcall func1(__int64 a1, __int64 a2, __int64 a3, __int64 a4)
{
__int64 v7; // rbx
int v8; // edi
char v9; // al
_QWORD *v10; // rbp
__int64 v12; // rax
unsigned int v13; // eax
__int64 v14; // rbp

v7 = 0LL;
v8 = *(_DWORD *)a1;
v9 = *(_BYTE *)(a1 + 4);
if ( v8 >= 0 )
{
if ( !v9 )
return a1;
do
{
LABEL_3:
v10 = (_QWORD *)(*(_QWORD *)(a1 + 8) + 8 * v7++);
*v10 = func1(*v10, a2, a3, a4);
}
while ( *(unsigned __int8 *)(a1 + 4) > (int)v7 );
return a1;
}
if ( v9 )
goto LABEL_3;
v12 = sn_to_str((unsigned int)-v8);
if ( (unsigned int)string_member_plist(v12, a4) )
return a1;
v13 = position_of_term_in_tlist(a1, a2);
if ( v13 == -1 )
return a1;
v14 = ith_in_plist(a3, v13);
zap_term(a1);
return copy_term(v14);
}

original_code:
static
Term subst_terms(Term t, Plist vars, Plist terms, Plist qvars)
{
  if (((t)->private_symbol < 0 && (t)->arity == 0)) {
    if (!string_member_plist(sn_to_str((-((t)->private_symbol))), qvars)) {
      int i = position_of_term_in_tlist(t, vars);
      if (i != -1) {
 Term corresponding_term = ith_in_plist(terms, i);
 zap_term(t);
 t = copy_term(corresponding_term);
      }
    }
    return t;
  }
  else {
    int i;
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = subst_terms(((t)->args[i]), vars, terms, qvars);
    return t;
  }
}

canonical_original_code:
static struct term *subst_terms(struct term *t, struct plist *vars, struct plist *terms, struct plist *qvars)
{
  if (((t)->private_symbol < 0 && (t)->arity == 0)) {
    if (!string_member_plist(sn_to_str((-((t)->private_symbol))), qvars)) {
      int i = position_of_term_in_tlist(t, vars);
      if (i != -1) {
 struct term *corresponding_term = ith_in_plist(terms, i);
 zap_term(t);
 t = copy_term(corresponding_term);
      }
    }
    return t;
  }
  else {
    int i;
    for (i = 0; i < ((t)->arity); i++)
      ((t)->args[i]) = subst_terms(((t)->args[i]), vars, terms, qvars);
    return t;
  }
}

variable_types:
t
struct term *

variable_types:
terms
struct plist *

variable_types:
qvars
struct plist *

variable_types: struct term { int private_symbol; unsigned char arity; unsigned char private_flags; struct term **args; void *container; union { unsigned int id; void *vp; } u; } *


decompiled_code:
int p_pindex_mem()
{
return fprint_pindex_mem(stdout, 1);
}

canonical_decompiled_code:
int func4()
{
return func3(stdout, 1);
}

original_code:
void p_pindex_mem()
{
  fprint_pindex_mem(stdout, TRUE);
}