def_module_params('combined_solver',
description='combines two solvers: non-incremental (solver1) and incremental (solver2)',
export=True,
params=(('solver2_timeout', UINT, UINT_MAX, "fallback to solver 1 after timeout even when in incremental model"),
('ignore_solver1', BOOL, False, "if true, solver 2 is always used"),
('solver2_unknown', UINT, 1, "what should be done when solver 2 returns unknown: 0 - just return unknown, 1 - execute solver 1 if quantifier free problem, 2 - execute solver 1")
))