Problem with DeltaSMT

[Jean Christoph Jung]

Hi all,
I started to use the DeltaSMT tool now and had problems to apply it to
other
instances than the examples. Here is what I did:

deltasmt -v -v -v examples/ex1.smt reduced.smt examples/run1.sh

This is the example from the README and it ran through as expected.
Then I copied "nextpoweroftwo128.smt" in the examples directory and
tried

deltasmt -v -v -v examples/nextpoweroftwo128.smt reduced.smt examples/
run1.sh

The output was:
file size of original formula: 55129 bytes
computing golden exit code: 0
parsing original formula
exception occurred: 2:1 expected: )

Has anybody had the problem before? Or does know where it might come
from?

best regards,
Jean

(My PC: AMD Athlon(tm) 64 X2 Dual Core Processor 6000+, java 1.6.0
(OpenJDK))

[Alberto Griggio]

Hello,

[...]

> deltasmt -v -v -v examples/nextpoweroftwo128.smt reduced.smt examples/
> run1.sh
>
> The output was:
> file size of original formula: 55129 bytes
> computing golden exit code: 0
> parsing original formula
> exception occurred: 2:1 expected: )
>
> Has anybody had the problem before? Or does know where it might come
> from?

I think this is the same problem that I had (see the message
http://groups.google.com/group/smt-tools/browse_thread/thread/69ab10e4a89a6c13).
I submitted a patch for this to Robert, hopefully he will find the
time to review it, fix it, and apply...

The problem is DeltaSMT has troubles in parsing some of the attributes
of benchmarks (at least :source, :status, :category). A workaround is
to manually remove them from the smt file before calling deltasmt,

Alberto

[Robert Brummayer]

I think Alberto is right. It should only need a minor fix in the
parser. I will look at Alberto's patch and release a new version as
soon as possible. In the meanwhile, as Alberto already pointed out,
simply remove attributes such as category, status, etc.

Best,
Robert

On 30 Sep., 16:02, Alberto Griggio <alberto.grig...@gmail.com> wrote:
> Hello,
>
> [...]
>
> > deltasmt -v -v -v examples/nextpoweroftwo128.smt reduced.smt examples/
> > run1.sh
>
> > The output was:
> > file size of original formula: 55129 bytes
> > computing golden exit code: 0
> > parsing original formula
> > exception occurred: 2:1 expected: )
>
> > Has anybody had the problem before? Or does know where it might come
> > from?
>

> I think this is the same problem that I had (see the messagehttp://groups.google.com/group/smt-tools/browse_thread/thread/69ab10e...).

[Robert Brummayer]

Hi Jean,

the new release (0.2) should fix your problem.

Best,
Robert

On 30 Sep., 22:43, Robert Brummayer <robert.brumma...@gmail.com>
wrote:

[Jean Christoph Jung]

Alberto, last night I realized that you had the same problem like me,
thanks for your help and the new version!

kind regards,
Jean

On Oct 1, 9:16 am, Robert Brummayer <robert.brumma...@gmail.com>
wrote: