Repository navigation

solve offline

Jump to bottom Edit New page

Aggelos Giantsios edited this page Oct 8, 2016 · 2 revisions

Solving constraints offline

An important ability, when dealing with bugs involving the solver, is to load recorded trace files offline and solve them.

This is possible with the following steps:

Comment out the macro DELETE_TRACE in cuter_macros.hrl and recompile CutEr.
Run CutEr. The recorded traces are the run.trace files in the temp directory and its sub-directories.
Solve a trace offline with cuter_solve_offline.py. Its usage follows.

Usage: cuter_solve_offline.py TraceFile NoOfConstraint [ options ]
PARAMETERS
	TraceFile		The trace file of an execution.
	NoOfConstraint		The cardinality of the constraint to reverse.
OPTIONS
	--print-constraints	Print all the commands as they are being loaded (for debugging).
	--smt			Uses the SMT backend.
	--help			Display this information.