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.stanford.edu/wiki/ ...and the Developer's Guide: https://github.com/CVC4/CVC4/wiki/Developer-Guide which contains coding guidelines for the CVC4 project. Good luck, and please contact cvc4-devel@cs.stanford.edu for assistance should you need it!