Commit 69710647 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Make sure the query in the SMTLIB result is set. 

SMTLIB's test suite ignored the Query parameter.  To avoid possible failures
in the future, stick a quick set of tests in for that.
parent ab50b843

src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerTest.java

+3 −0
Original line number Diff line number Diff line
@@ -38,6 +38,7 @@ import org.junit.runners.JUnit4; 


import java.util.List;



import static org.hamcrest.CoreMatchers.is;

import static org.junit.Assert.*;



/**
@@ -66,10 +67,12 @@ public class CheckerRunnerTest { 
        assertEquals(2, res.get(0).SampleValues.size());

        assertEquals("0.0", res.get(0).SampleValues.get("x"));

        assertEquals("1.0", res.get(0).SampleValues.get("z"));

        assertThat(res.get(0).Query, is("(assert (and (= x 0.0) (or (and (> z 0.0) (= z 1.0))\n(and (> z 0.0) (> 0.0 z))\n(and (= z 1.0) (> 0.0 z)))))"));



        assertEquals(2, res.get(1).SampleValues.size());

        assertEquals("0.0", res.get(1).SampleValues.get("x"));

        assertEquals("0.0", res.get(1).SampleValues.get("z"));

        assertThat(res.get(1).Query, is("(assert (and (= x 0.0) (not (or (> z 0.0) (= z 1.0) (> 0.0 z)))))"));

    }

    @Test

    public void TestRunningZ3WithNegative() {