2005-07-26  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/formula.ml, cvcl/formula.mli, cvcl/skolemizer.ml, cvcl/skolemizer.mli, cvcl/smt/expressions.ml, cvcl/smt/parser_helper.ml, cvcl/smt/smt_parser.mly, cvcl/term_db.ml, cvcl/term_db.mli, dpllt.ml:
	modified the structures and procedures to do instantiation of a quantified formula completely rather than just the topmost quantifier prefix

2005-07-23  Jed Hagen  <ghagen@cs.uiowa.edu>

	* zolc/convert.ml, zolc/global.ml: zolc tweaks

2005-07-22  Eric Collins  <elcollin@cs.uiowa.edu>

	* zolc/constr.ml, zolc/convert.ml, zolc/theory.ml:
	Uses the new Pred.ml function set_quantified_abstract to flag objective variables
	Relies on the global.pars.only_positive_quantified_abstract something or other to only use objective variables set to one
	Line 29 in convert.ml had to be re-uncommented to compile.  I'm not sure what that means.
	This version has a bug.

2005-07-22  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/global.ml, pred_db.ml, zolc/global.ml:
	flag to limit quantified lemma in pred_db

	* cvcl/theory.ml, pred.ml, pred.mli, zolc/convert.ml:
	quantified abstraction flag in preds is now mutable with accessor

2005-07-20  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/convert.ml, cvcl/global.ml, cvcl/skolemizer.ml, dpllt.ml:
	Removed debugging statements accidentally left in in the last update.

	* cvcl/smt/Makefile, cvcl/smt/expressions.ml, cvcl/smt/main.ml, cvcl/smt/parser_helper.ml, cvcl/smt/parser_helper.mli, cvcl/smt/smt_lexer.mll, cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.ml, cvcl/api_native.ml, cvcl/convert.ml, cvcl/formula.ml, cvcl/formula.mli, cvcl/global.ml, cvcl/skolemizer.ml, cvcl/skolemizer.mli, cvcl/term_db.ml, cvcl/term_db.mli:
	created new module for the term database, term_db.
	Seperated the term generation from the instantiation procedure.
	modified the freevar list to associate the sort id with each variable in the list

	* dpllt.ml, pred_db.ml, pred_db.mli:
	removed the term database from pred_db and moved it to a new module, term_db

2005-07-12  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/theory.ml: fixed changed_preds to actually do something

	* cvcl/theory_w.cpp: put appFloor behind ifdefs

2005-07-11  Eric Collins  <elcollin@cs.uiowa.edu>

	* zolc/constr.ml, zolc/global.ml, zolc/theory.ml:
	Optimization is close to working, theory.ml uses "bubble up" technique on
	backtracking objective variables implicated to zero.

2005-07-09  Jed Hagen  <ghagen@cs.uiowa.edu>

	* INSTALL, cvcl/global.ml, dpllt.ml, zolc/global.ml:
	minor modifications

	* pred.ml:
	altered pred.ml in anticipation of supporting an array of theories

2005-07-08  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/main.ml, cvcl/smt/smt_parser.mly, dpllt.ml, satbox.ml:
	re-enable stuff after the smtcomp

2005-07-05  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/theories.ml, dpllt.ml, satbox.ml, satbox/proto.h, satbox/util.c:
	removed model check for the moment

2005-07-04  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/theories.ml: theories update

	* cvcl/smt/main.ml, cvcl/theory.ml, cvcl/theory_w.cpp:
	allows new version of cvcl

2005-07-03  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/global.ml, cvcl/satbox_in.cpp, cvcl/smt/expressions.ml, cvcl/theory.ml, dpllt.ml, pred_db.ml, satbox.ml:
	model checking stuff

2005-07-02  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/main.ml, cvcl/smt/smt_parser.mly:
	modifying main.ml to allow input from stdin

	* satbox/proto.h, satbox/util.c: removing more conflicts

	* satbox/main.c: removing extra definition of dpllt_reason_satbox

	* new_theory/EXTENDING, EXTENDING, INSTALL, cvcl/smt/README.TXT:
	modifying readmes

	* AUTHORS, cvcl/cstore_old.ml, cvcl/dce.ml, cvcl/dce.mli, cvcl/escjava_label.ml, cvcl/escjava_label.mli, cvcl/satbox_in.cpp, cvcl/smt/parser_helper.ml, cvcl/smt/theories.ml, cvcl/theory_w.cpp, satbox.ml, satbox.mli:
	modifying attributions

	* cvcl/interface/Makefile, cvcl/smt/Makefile: new makefiles

	* configure.pl, cvcl/interface/Makefile, cvcl/smt/Makefile, cvcl/smt/Makefile.in:
	new makefiles, configure script

	* cvcl/smt/Makefile, cvcl/smt/Makefile.in, cvcl/interface/Makefile, cvcl/interface/Makefile.in:
	makefile tweaks

	* cvcl/smt/Makefile, cvcl/smt/Makefile.in, cvcl/interface/Makefile, cvcl/interface/Makefile.in:
	new Makefile.in

	* cvcl/smt/Makefile.in: makefile for the masses

2005-07-01  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/cstore.ml, cvcl/escjava_label.ml, cvcl/formula.ml, cvcl/skolemizer.ml, cvcl/smt/theory_db.ml, cvcl/theory.ml, pqueue.ml, pred.ml:
	== temporarily replaced with '  =  '

2005-06-28  Eric Collins  <elcollin@cs.uiowa.edu>

	* zolc/constr.ml, zolc/pbs_lexer.mll, zolc/pbs_parser.mly, zolc/theory.ml:
	Same as last time, only with the updates to the pbs parser to work with objective function

2005-06-27  Eric Collins  <elcollin@cs.uiowa.edu>

	* zolc/cstore.ml, zolc/skolemizer.ml, zolc/theory.ml, zolc/theory.mli:
	Should be a mostly working version of the optimizer.
	This uses the original way of causing a backtrack (all preds in the current model are
	incorporated in the new lemma)

	-Eric (june 27th)

2005-06-26  Jed Hagen  <ghagen@cs.uiowa.edu>

	* zolc/global.ml, cvcl/convert.ml, cvcl/global.ml, cvcl/interface/Makefile, cvcl/smt/Makefile, cvcl/smt/expressions.ml, dpllt.ml, pqueue.ml, pqueue.mli, pred.ml, pred.mli, satbox.mli, sys_state.ml:
	changed use of Global.append_list, tweaked next_lit

2005-06-25  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/smt_parser.mly: correcting output for no_negate_queries

2005-06-23  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/cstore.ml, cvcl/formula.ml, cvcl/smt/expressions.ml, cvcl/theory.ml, dpllt.ml, pqueue.ml, pred.ml, pred_db.ml, satbox.ml:
	rejecting current model only based on decision lits if non-quantified

2005-06-21  Jed Hagen  <ghagen@cs.uiowa.edu>

	* dpllt.ml: error in eliminating model fixed

	* zolc/Makefile, zolc/api_native.ml, zolc/convert.ml, zolc/convert.mli, zolc/escjava_label.ml, zolc/escjava_label.mli:
	bringing in line with changes elsewhere

	* cvcl/api_native.ml, cvcl/api_native.mli, cvcl/convert.ml, cvcl/convert.mli, cvcl/escjava_label.ml, cvcl/escjava_label.mli, cvcl/skolemizer.ml, cvcl/smt/Makefile, cvcl/smt/api_xml.ml, cvcl/smt/main.ml, cvcl/smt/smt_parser.mly, dpllt.ml, iset.ml, iset.mli, pqueue.ml, pred.ml, pred.mli, pred_db.ml:
	removing extra stuff in pred.ml

2005-06-19  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/smt/expressions.ml: fixed the guard in formula ite's

	* cvcl/api_native.ml, cvcl/escjava_label.ml, cvcl/escjava_label.mli, cvcl/formula.ml, cvcl/formula.mli, cvcl/global.ml, cvcl/skolemizer.ml, cvcl/skolemizer.mli, cvcl/smt/Makefile, cvcl/smt/expressions.ml, cvcl/smt/expressions.mli, cvcl/smt/main.ml, cvcl/smt/parser_helper.ml, cvcl/smt/smt_parser.mly, pred.ml, pred.mli:
	added code to record depth of predicates, and code to mark guarded predicates, and storing label information

2005-06-16  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/global.ml, dpllt.ml, zolc/global.ml, zolc/main.ml:
	allow disallowing exact models on exhausted case

2005-06-15  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/cstore.ml, cvcl/cvc/api_xml.ml, cvcl/cvc/cvc_command_parser.mly, cvcl/cvc/cvc_parser.mly, cvcl/cvc/main.ml, cvcl/cvc/parser_helper.ml, cvcl/formula.ml, cvcl/global.ml, cvcl/sammy_httpd.ml, cvcl/smt/smt_parser.mly, cvcl/smt/theories.ml, cvcl/theory.ml, pqueue.ml, pred.ml, pred_db.ml, satbox.ml, zolc/api_native.ml, zolc/constr.ml, zolc/cstore.ml, zolc/dimacs_parser.mly, zolc/global.ml, zolc/main.ml, zolc/mps_parser.mly, zolc/pbs_parser.mly, dpllt.ml:
	changed debug statements to a hopefully more runtime-friendly method

2005-06-14  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/skolemizer.ml:
	modified random seed printout only on verbose -- made it a bit safer :)

	* cvcl/skolemizer.ml: modified random seed printout only on verbose

	* cvcl/smt/smt_lexer.mll: tweak to lexer to allow apostrophies in names

	* cvcl/theory_w.cpp: moved tests to deebug only

2005-06-11  Eric Collins  <elcollin@cs.uiowa.edu>

	* zolc/constr.ml, zolc/theory.ml:
	constr.ml has been updated to remove any unnecessary clauses
	theory.ml has had a few bugs removed

2005-06-10  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/global.ml, cvcl/skolemizer.ml, pred.ml, pred.mli, zolc/global.ml:
	added global flags to support additional split heuristics, also added and/or decision preferences

	* zolc/main.ml: mnior change in main to fix pbs file extensions

2005-06-06  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/satbox_in.cpp, cvcl/smt/smt_lexer.mll, cvcl/smt/smt_parser.mly:
	slight changes to lexer, parser, also upped max_preds in satbox_in

2005-06-05  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/smt/theories.ml:
	Added the QF_UFLIA theory with numerals assumed to be ints

2005-06-05  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/smt_lexer.mll: allow single quotes in identifiers

	* cvcl/smt/expressions.ml, cvcl/smt/smt_lexer.mll, cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.ml:
	added ~ (unary minus) to interpreted sunction symbols

	* cvcl/smt/smt_parser.mly:
	use Parser_helper.compare_sorts in ite expressions

2005-06-03  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/Makefile, dpllt.ml, satbox.ml, satbox.mli: resynch

2005-05-23  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.ml, dpllt.ml:
	correctly caught sortNotFound exception in theory_db

	* cvcl/cvc/parser_helper.ml, cvcl/theory.ml, cvcl/theory.mli, cvcl/theory_w.cpp:
	added functionality to get type ids from cvcl

	* cvcl/smt/main.ml, cvcl/theory_w.cpp: resynch

2005-05-21  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/smt/expressions.ml, cvcl/smt/smt_parser.mly, cvcl/smt/theories.ml, cvcl/smt/theory_db.ml, cvcl/smt/theory_db.mli:
	fixed the built in array definitions for QF_AUFLIA

2005-05-21  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/smt/parser_helper.ml, cvcl/smt/theory_db.ml:
	adding Not_found checks

	* cvcl/api_native.ml, cvcl/global.ml, cvcl/smt/smt_parser.mly, dpllt.ml:
	fixed stupid error in api_native & verbose

2005-05-19  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.mli:
	added some debug info

2005-05-19  Jed Hagen  <ghagen@cs.uiowa.edu>

	* pqueue.ml, pred.ml, pred.mli:
	prep for adding guard & formua depth flags to preds

2005-05-19  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/smt/Makefile, cvcl/smt/smt_parser.mly, cvcl/smt/theories.ml, cvcl/smt/theory_db.ml, cvcl/smt/theory_db.mli:
	made the theory_db work better for handling different theories

2005-05-19  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/api_native.ml, cvcl/smt/main.ml, cvcl/smt/smt_parser.mly:
	playing with formula negations

2005-05-18  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/global.ml, pqueue.ml, zolc/global.ml, zolc/main.ml, zolc/skolemizer.ml:
	adding nonwatched_lits_last flag

2005-05-17  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/cstore.ml, cvcl/cstore.mli, zolc/cstore.ml, zolc/skolemizer.ml:
	starting to change zolc for optimizer

	* zolc/theory.ml: theory update

2005-05-17  Michael DeCoster  <mdecoste@cs.uiowa.edu>

	* cvcl/smt/expressions.ml:
	declares interpreted predicates to the pred_db now

2005-05-17  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/global.ml, cvcl/smt/parser_helper.ml, cvcl/smt/parser_helper.mli, cvcl/smt/smt_parser.mly, cvcl/theory_w.cpp, pred_db.ml:
	added real=int comparison to smt parser_helper, looking for bugs

	* cvcl/.api_native.ml.swp, cvcl/satbox_in.cpp, cvcl/smt/Makefile, cvcl/smt/main.ml, cvcl/smt/parser_helper.ml, cvcl/smt/parser_helper.mli, cvcl/smt/smt_lexer.mll, cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.ml, cvcl/smt/theory_db.mli, cvcl/theory_w.cpp, satbox/array.h, satbox/main.c, satbox/main.h, satbox/proto.h, satbox/satbox.c, satbox/satbox.h, satbox/sato.c, satbox/tape.h, satbox/util.c, satbox/weight.h:
	fixes against smtcomp

2005-05-14  Jed Hagen  <ghagen@cs.uiowa.edu>

	* cvcl/cvc/Makefile, cvcl/cvc/main.ml: getting it to work

2005-05-13  Jed Hagen  <ghagen@cs.uiowa.edu>

	* AUTHORS, EXTENDING, INSTALL, LICENSE, c_array.ml, c_array.mli, client/ASL.txt, client/README, client/SammyCvcClient.java, client/SammySmtClient.java, client/xmlrpc-1.2-b1-modified.jar, configure.pl, counter.ml, cvcl/.api_native.ml.swp, cvcl/api_native.ml, cvcl/api_native.mli, cvcl/configure.scan, cvcl/convert.ml, cvcl/convert.mli, cvcl/cstore.ml, cvcl/cstore.mli, cvcl/cstore_old.ml, cvcl/cvc/Makefile, cvcl/cvc/api_xml.ml, cvcl/cvc/bcp.pl, cvcl/cvc/cvc_command_lexer.mll, cvcl/cvc/cvc_command_parser.mly, cvcl/cvc/cvc_lexer.mll, cvcl/cvc/cvc_parser.mly, cvcl/cvc/dimacs2cvc.pl, cvcl/cvc/dimacs_lexer.mll, cvcl/cvc/dimacs_parser.mly, cvcl/cvc/duplicates.pl, cvcl/cvc/main.ml, cvcl/cvc/parser_helper.ml, cvcl/cvc/parser_helper.mli, cvcl/cvc/readme.txt, cvcl/dce.ml, cvcl/dce.mli, cvcl/formula.ml, cvcl/formula.mli, cvcl/global.ml, cvcl/interface/Makefile, cvcl/interface/Makefile.in, cvcl/interface/config.h, cvcl/interface/configure.scan, cvcl/interface/theory_w.h, cvcl/sammy_httpd.ml, cvcl/sammy_xml.idl, cvcl/satbox_in.cpp, cvcl/skolemizer.ml, cvcl/skolemizer.mli, cvcl/smt/Makefile, cvcl/smt/Makefile.cl, cvcl/smt/Makefile.sv, cvcl/smt/README.TXT, cvcl/smt/api_xml.ml, cvcl/smt/api_xml.mli, cvcl/smt/basic_expression.ml, cvcl/smt/basic_expression.mli, cvcl/smt/expressions.ml, cvcl/smt/expressions.mli, cvcl/smt/main.ml, cvcl/smt/parser_helper.ml, cvcl/smt/parser_helper.mli, cvcl/smt/server.ml, cvcl/smt/smt_lexer.mll, cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.ml, cvcl/smt/theory_db.mli, cvcl/theory.ml, cvcl/theory.mli, cvcl/theory_w.cpp, dpllt.ml, dpllt.mli, iset.ml, iset.mli, new_theory/EXTENDING, new_theory/global.ml, new_theory/smt/Makefile, new_theory/theory.ml, new_theory/theory.mli, pqueue.ml, pqueue.mli, pred.ml, pred.mli, pred_db.ml, pred_db.mli, reduce.ml, reduce.mli, satbox.ml, satbox.mli, satbox/1.sbx, satbox/array.h, satbox/clocks.h, satbox/common.h, satbox/main.c, satbox/main.h, satbox/makefile, satbox/makeg, satbox/proto.h, satbox/readme.sbx, satbox/satbox.c, satbox/satbox.h, satbox/sato.c, satbox/sato.h, satbox/select.h, satbox/tape.h, satbox/trie.c, satbox/trie.h, satbox/util.c, satbox/vstack.h, satbox/weight.h, state.ml, state.mli, sys_state.ml, sys_state.mli, xor/._ncdi/api_native.di, xor/._ncdi/convert.di, xor/._ncdi/dce.di, xor/._ncdi/dimacs_parser.di, xor/._ncdi/ifip_parser.di, xor/Makefile, xor/README, xor/api_native.ml, xor/api_native.mli, xor/convert.ml, xor/convert.mli, xor/cstore.ml, xor/cstore.mli, xor/dce.ml, xor/dce.mli, xor/dce2.ml, xor/dimacs_lexer.ml, xor/dimacs_lexer.mll, xor/dimacs_parser.ml, xor/dimacs_parser.mli, xor/dimacs_parser.mly, xor/empty_theory.ml, xor/extract.ml, xor/global.ml, xor/gmon.out, xor/ifip015werner.txt, xor/ifip_lexer.ml, xor/ifip_lexer.mll, xor/ifip_parser.ml, xor/ifip_parser.mli, xor/ifip_parser.mly, xor/main.ml, xor/profile.txt, xor/profile_uf200-03_dynamic_extra_no_theory.txt, xor/profile_uf200-03_no_extra_no_theory.txt, xor/skolemizer.ml, xor/theory.ml, xor/theory.mli, xor/timetable, zolc/Makefile, zolc/OCamlMakefile, zolc/api_native.ml, zolc/api_native.mli, zolc/constr.ml, zolc/convert.ml, zolc/convert.mli, zolc/cstore.ml, zolc/cstore.mli, zolc/dce.ml, zolc/dce.mli, zolc/dimacs_lexer.mll, zolc/dimacs_parser.mly, zolc/global.ml, zolc/ifip_lexer.mll, zolc/ifip_parser.mly, zolc/interface/Makefile, zolc/interface/Makefile.in, zolc/interface/compat_hash_map.h, zolc/interface/config.h, zolc/interface/configure.scan, zolc/interface/theory_w.h, zolc/main.ml, zolc/mps_lexer.mll, zolc/mps_parser.mly, zolc/opb_lexer.mll, zolc/opb_parser.mly, zolc/pbs_lexer.mll, zolc/pbs_parser.mly, zolc/satbox_in.cpp, zolc/skolemizer.ml, zolc/theory.ml, zolc/theory.mli:
	New file.

	* AUTHORS, EXTENDING, INSTALL, LICENSE, c_array.ml, c_array.mli, client/ASL.txt, client/README, client/SammyCvcClient.java, client/SammySmtClient.java, client/xmlrpc-1.2-b1-modified.jar, configure.pl, counter.ml, cvcl/.api_native.ml.swp, cvcl/api_native.ml, cvcl/api_native.mli, cvcl/configure.scan, cvcl/convert.ml, cvcl/convert.mli, cvcl/cstore.ml, cvcl/cstore.mli, cvcl/cstore_old.ml, cvcl/cvc/Makefile, cvcl/cvc/api_xml.ml, cvcl/cvc/bcp.pl, cvcl/cvc/cvc_command_lexer.mll, cvcl/cvc/cvc_command_parser.mly, cvcl/cvc/cvc_lexer.mll, cvcl/cvc/cvc_parser.mly, cvcl/cvc/dimacs2cvc.pl, cvcl/cvc/dimacs_lexer.mll, cvcl/cvc/dimacs_parser.mly, cvcl/cvc/duplicates.pl, cvcl/cvc/main.ml, cvcl/cvc/parser_helper.ml, cvcl/cvc/parser_helper.mli, cvcl/cvc/readme.txt, cvcl/dce.ml, cvcl/dce.mli, cvcl/formula.ml, cvcl/formula.mli, cvcl/global.ml, cvcl/interface/Makefile, cvcl/interface/Makefile.in, cvcl/interface/config.h, cvcl/interface/configure.scan, cvcl/interface/theory_w.h, cvcl/sammy_httpd.ml, cvcl/sammy_xml.idl, cvcl/satbox_in.cpp, cvcl/skolemizer.ml, cvcl/skolemizer.mli, cvcl/smt/Makefile, cvcl/smt/Makefile.cl, cvcl/smt/Makefile.sv, cvcl/smt/README.TXT, cvcl/smt/api_xml.ml, cvcl/smt/api_xml.mli, cvcl/smt/basic_expression.ml, cvcl/smt/basic_expression.mli, cvcl/smt/expressions.ml, cvcl/smt/expressions.mli, cvcl/smt/main.ml, cvcl/smt/parser_helper.ml, cvcl/smt/parser_helper.mli, cvcl/smt/server.ml, cvcl/smt/smt_lexer.mll, cvcl/smt/smt_parser.mly, cvcl/smt/theory_db.ml, cvcl/smt/theory_db.mli, cvcl/theory.ml, cvcl/theory.mli, cvcl/theory_w.cpp, dpllt.ml, dpllt.mli, iset.ml, iset.mli, new_theory/EXTENDING, new_theory/global.ml, new_theory/smt/Makefile, new_theory/theory.ml, new_theory/theory.mli, pqueue.ml, pqueue.mli, pred.ml, pred.mli, pred_db.ml, pred_db.mli, reduce.ml, reduce.mli, satbox.ml, satbox.mli, satbox/1.sbx, satbox/array.h, satbox/clocks.h, satbox/common.h, satbox/main.c, satbox/main.h, satbox/makefile, satbox/makeg, satbox/proto.h, satbox/readme.sbx, satbox/satbox.c, satbox/satbox.h, satbox/sato.c, satbox/sato.h, satbox/select.h, satbox/tape.h, satbox/trie.c, satbox/trie.h, satbox/util.c, satbox/vstack.h, satbox/weight.h, state.ml, state.mli, sys_state.ml, sys_state.mli, xor/._ncdi/api_native.di, xor/._ncdi/convert.di, xor/._ncdi/dce.di, xor/._ncdi/dimacs_parser.di, xor/._ncdi/ifip_parser.di, xor/Makefile, xor/README, xor/api_native.ml, xor/api_native.mli, xor/convert.ml, xor/convert.mli, xor/cstore.ml, xor/cstore.mli, xor/dce.ml, xor/dce.mli, xor/dce2.ml, xor/dimacs_lexer.ml, xor/dimacs_lexer.mll, xor/dimacs_parser.ml, xor/dimacs_parser.mli, xor/dimacs_parser.mly, xor/empty_theory.ml, xor/extract.ml, xor/global.ml, xor/gmon.out, xor/ifip015werner.txt, xor/ifip_lexer.ml, xor/ifip_lexer.mll, xor/ifip_parser.ml, xor/ifip_parser.mli, xor/ifip_parser.mly, xor/main.ml, xor/profile.txt, xor/profile_uf200-03_dynamic_extra_no_theory.txt, xor/profile_uf200-03_no_extra_no_theory.txt, xor/skolemizer.ml, xor/theory.ml, xor/theory.mli, xor/timetable, zolc/Makefile, zolc/OCamlMakefile, zolc/api_native.ml, zolc/api_native.mli, zolc/constr.ml, zolc/convert.ml, zolc/convert.mli, zolc/cstore.ml, zolc/cstore.mli, zolc/dce.ml, zolc/dce.mli, zolc/dimacs_lexer.mll, zolc/dimacs_parser.mly, zolc/global.ml, zolc/ifip_lexer.mll, zolc/ifip_parser.mly, zolc/interface/Makefile, zolc/interface/Makefile.in, zolc/interface/compat_hash_map.h, zolc/interface/config.h, zolc/interface/configure.scan, zolc/interface/theory_w.h, zolc/main.ml, zolc/mps_lexer.mll, zolc/mps_parser.mly, zolc/opb_lexer.mll, zolc/opb_parser.mly, zolc/pbs_lexer.mll, zolc/pbs_parser.mly, zolc/satbox_in.cpp, zolc/skolemizer.ml, zolc/theory.ml, zolc/theory.mli:
	sammy satbox import

