Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
Mon, 14 Feb 2011 12:25:26 +0100 |
boehmes |
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
|
file |
diff |
annotate
|
Mon, 14 Feb 2011 10:40:43 +0100 |
boehmes |
more explicit errors to inform users about problems related to SMT solvers;
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 18:58:54 +0100 |
boehmes |
be more precise: also merge option values
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 17:41:45 +0100 |
boehmes |
only print warning in a visible context (previously, the warning was printed more than once)
|
file |
diff |
annotate
|
Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 13:24:09 +0100 |
boehmes |
shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 09:26:27 +0100 |
boehmes |
made SML/NJ happy
|
file |
diff |
annotate
|
Thu, 06 Jan 2011 17:51:56 +0100 |
boehmes |
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to enable trigger inference;
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
moved SMT classes and dictionary functions to SMT_Utils
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 08:39:24 +0100 |
boehmes |
added option to modify the random seed of SMT solvers
|
file |
diff |
annotate
|
Tue, 07 Dec 2010 14:53:12 +0100 |
boehmes |
centralized handling of built-in types and constants;
|
file |
diff |
annotate
|
Wed, 17 Nov 2010 08:14:55 +0100 |
boehmes |
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
|
file |
diff |
annotate
|
Fri, 12 Nov 2010 15:56:07 +0100 |
boehmes |
look for certificates relative to the theory
|
file |
diff |
annotate
|
Mon, 08 Nov 2010 12:13:44 +0100 |
boehmes |
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
|
file |
diff |
annotate
|