test(setlogic) :-
parse_smtlib2("(set-logic AUFLIA)",Tree), !,
Tree == [set_logic('AUFLIA')].
test(setinfo_version) :-
parse_smtlib2("(set-info :smt-lib-version 2.0)",Tree), !,
Tree == [set_info(attribute('smt-lib-version',decimal(2.0)))].
test(setinfo_source_multiline) :-
parse_smtlib2("(set-info :source |\nOlder mathsat benchmarks. Contact Mathsat group at http://mathsat.itc.it/ for\nmore information.\n\nThis benchmark was automatically translated into SMT-LIB format from\nCVC format using CVC Lite\n|)",Tree),
Tree == [set_info(attribute(source,string('\nOlder mathsat benchmarks. Contact Mathsat group at http://mathsat.itc.it/ for\nmore information.\n\nThis benchmark was automatically translated into SMT-LIB format from\nCVC format using CVC Lite\n')))].
test(setinfo_category_string) :-
parse_smtlib2("(set-info :category \"industrial\")",Tree),
Tree == [set_info(attribute(category,string(industrial)))].
test(declare1) :-
parse_smtlib2("(declare-fun boolIff (Int Int) Int)",Tree), !,
Tree == [declare_fun('boolIff',[sort('Int'),sort('Int')],sort('Int'))].
test(assertion1) :-
parse_smtlib2("(assert (not (= (IsDirectlyModifiableField allocated_) Smt.true)))",Tree), !,
Tree == [assert(id_term(id(not),[id_term(id(=),[id_term(id('IsDirectlyModifiableField'),[id(allocated_)]),id('Smt.true')])]))].
test(assertion2_nocomment) :-
parse_smtlib2("(assert (forall ((?c Int)) (= (ClassReprInv (ClassRepr ?c)) ?c)))", Tree), !,
Tree == [assert(forall([svar('?c',sort('Int'))],id_term(id(=),[id_term(id('ClassReprInv'),[id_term(id('ClassRepr'),[id('?c')])]),id('?c')])))].
test(assertion2) :-
parse_smtlib2("(assert (forall ((?c Int)) (! (= (ClassReprInv (ClassRepr ?c)) ?c) :pattern ((ClassRepr ?c)) )))", Tree), !,
Tree == [assert(forall([svar('?c',sort('Int'))],attributed_term(id_term(id('='),[id_term(id('ClassReprInv'),[id_term(id('ClassRepr'),[id('?c')])]),id('?c')]),[attribute(pattern,[['ClassRepr','?c']])])))].
test(array_declaration) :-
parse_smtlib2("(declare-fun a_75 () (Array Index Element))", Tree), !,
Tree == [declare_fun(a_75,[],sort('Array',[sort('Index'),sort('Element')]))].