A modified version of FuzzSMT to output SMTLIB2 format.

37 views
Skip to first unread message

Trevor Hansen

unread,
Feb 3, 2011, 12:15:26 AM2/3/11
to SMT Tools
Hello,

Some of you may be interested that I've created a modified version of
FuzzSMT. I've given it the version number of 0.3.1. It is different
from the 0.2 version in that :
* It outputs SMTLIB2 format by default.
* It adds the QF_ABV logic.
* It adds the -bulk-export and -bulk-prefix flags. This allows you to
call it like this (say):

./fuzzsmt QF_ABV -bulk-prefix run1 -bulk-export 1000

This will create 1000 files named: run1_file_[0..999].smt2. Creating
1000 files in one go is much faster than calling FuzzSMT 1000 times.
FuzzSMT is written in Java, meaning the java virtual machine needs to
load each time FuzzSMT is run. Loading the JVM is costly. To create
1000 instances via the standard invocation:

./fuzzsmt QF_ABV

Takes about 120 seconds, with the -bulk-export option it takes about 3
seconds.

The -bulk-prefix is to allow multiple processes to create instances in
the same directory, by for example using the process identification
number as the prefix.

Here is a link: http://www.csse.unimelb.edu.au/~thansen/fuzzsmt-0.3.1.tar.bz2

Please let me know if something looks wrong.

Best,

Trevor.



Reply all
Reply to author
Forward
0 new messages