Congratulations, you now have a new theory of $dir ! Your next steps will likely be: * to implement a decision procedure for your theory by implementing Theory$camel::check() in theory_$dir.cpp. Before writing the actual code, you will need : * to determine which data structures are context dependent and use for them context-dependent data structures (context/cd*.h) * to choose which work will be done at QUICK_CHECK, STANDARD or at FULL_EFFORT. You'll probably find the Developer's wiki useful: http://cvc4.cs.nyu.edu/wiki/ ...and in particular the Developer's Guide: http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide which contains coding guidelines for the CVC4 project. Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance should you need it!