An Emacs major mode to edit and run SMTLIB v2 files
This mode is based on lisp-mode and provides highlighting of SMTLIB v2 commands, as well as the command run-solver (bound to C-c C-c) to run an SMT solver on the buffer or the region.
Add the following lines to your .emacs
(setq auto-mode-alist (cons '("\\.smt2$" . smtlib-mode) auto-mode-alist))
(autoload 'smtlib-mode "smtlib" "Major mode for SMTLIB" t)
The command to run the SMT solver is by default "cvc4 --lang smt2", modify and add the following line to your .emacs to change.
(setq smtlib-solver-cmd "cvc4 --lang smt2")