diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg
new file mode 100644
index 000000000..689519e6c
--- /dev/null
+++ b/src/model/model_params.pyg
@@ -0,0 +1,9 @@
+def_module_params('model', 
+                  export=True,
+                  params=(('validate', BOOL, False, 'validate models produced by Z3'),
+                          ('partial', BOOL, False, 'enable/disable partial function interpretations'),
+                          ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
+                          ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
+                          ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
+                          ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model')))
+