Path: . Working Copy Root Path: /Users/tester/work/sarl/mile2/r1162 URL: svn://vsl.cis.udel.edu/sarl/tags/mile2 Relative URL: ^/tags/mile2 Repository Root: svn://vsl.cis.udel.edu/sarl Repository UUID: 7d651925-2d04-6a0e-8c93-cd1e20bcaab1 Revision: 1162 Node Kind: directory Schedule: normal Last Changed Author: siegel Last Changed Rev: 1162 Last Changed Date: 2013-10-30 08:48:21 -0400 (Wed, 30 Oct 2013)
Stdout:
Buildfile: /Users/tester/work/sarl/mile2/r1162/build.xml
compile:
[mkdir] Created dir: /Users/tester/work/sarl/mile2/r1162/bin
[javac] Compiling 219 source files to /Users/tester/work/sarl/mile2/r1162/bin
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/expr/cnf/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/expr/IF/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/collections/common/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/collections/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/preuniverse/common/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/collections/IF/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/prove/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/prove/IF/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/IF/expr/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/expr/common/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/prove/common/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/IF/type/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/prove/cvc/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/ideal/common/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/herbrand/common/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/expr/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/ideal/IF/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/IF/number/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/number/real/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/preuniverse/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/ideal/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/IF/object/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/IF/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/preuniverse/IF/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/number/package-info.class
[javac] Creating empty /Users/tester/work/sarl/mile2/r1162/bin/edu/udel/cis/vsl/sarl/herbrand/package-info.class
jar:
[jar] Building jar: /Users/tester/work/sarl/mile2/r1162/sarl.jar
test-init:
[mkdir] Created dir: /Users/tester/work/sarl/mile2/r1162/junit
[mkdir] Created dir: /Users/tester/work/sarl/mile2/r1162/junit/data
[mkdir] Created dir: /Users/tester/work/sarl/mile2/r1162/junit/reports
[mkdir] Created dir: /Users/tester/work/sarl/mile2/r1162/bin-test
test-compile:
[javac] Compiling 130 source files to /Users/tester/work/sarl/mile2/r1162/bin-test
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.ArrayTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.348 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] jagged1: a = a[0:=(int[2])<5,6>, 1:=(int[1])<17>]
[junit] arrayRead1: a = (int[2])<5,6>
[junit] array2d: new row is: a[0][0:=2]
[junit] b1 = a[2:=2, 4:=2]
[junit] b2 = a[2:=2, 4:=2]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.BooleanTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.017 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.CharTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.008 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] string: s1 = (CHAR[5])<'H','e','l','l','o'>
[junit] string: s2 = (CHAR[7])<' ','t','h','e','r','e','.'>
[junit] ab: a = 'a'
[junit] ab: b = 'b'
[junit] symbolic: eq: x == y
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.DemoTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 4, Time elapsed: 0.406 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] read = (real[3])<x,y,15707963/5000000>[i]
[junit] write = (real[3])<x,y,15707963/5000000>[i:=2]
[junit] readwrite : (real[3])<x,y,15707963/5000000>[i:=2][i]
[junit] readwrite simplfied: (real[3])<x,y,15707963/5000000>[i:=2][i]
[junit] Is readwrite=2? YES
[junit] ------------- ---------------- ---------------
[junit] Testcase: linear(edu.udel.cis.vsl.sarl.IF.DemoTest):SKIPPED
[junit] Testcase: exp(edu.udel.cis.vsl.sarl.IF.DemoTest):SKIPPED
[junit] Testcase: test(edu.udel.cis.vsl.sarl.IF.DemoTest):SKIPPED
[junit] Testcase: array(edu.udel.cis.vsl.sarl.IF.DemoTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.FindModelTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.086 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] array1: value = (int[1])<-1>
[junit] array2: value = (int[5])<0,0,0,0,0>
[junit] array3: value = (int[2])<-1,-2>
[junit] findX: X = -1/4
[junit] sqrt4: value = 2
[junit] completeArray : N_val = 1
[junit] completeArray : b_val = (int[1])<-1>
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.FloatModelTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.372 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] difference = e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(x1+x2)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(x1+x2)*x2+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x1+x2)*x1+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x1+x2)*x2+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x3+x4)*x3+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x3+x4)*x4+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x3+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x4+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x1+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x2+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x3+-1*e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x4+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+-1*e(x3+x4)*x3+-1*e(x3+x4)*x4
[junit] positivized = e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(x1+x2)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x3+x4)*x3+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*e(x3+x4)*x4+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x1+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x2+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x3+e(e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*e(x1+x2)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3+x4)*x4+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x3+e(e(x1+x2)*x1+e(x1+x2)*x2+e(x3+x4)*x3+e(x3+x4)*x4+x1+x2+x3+x4)*x4+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x1+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x2+e(e(x1+x2)*x1+e(x1+x2)*x2+x1+x2+x3)*x3+e(x3+x4)*x3+e(x3+x4)*x4
[junit] upperBound1 = (E^3)*x1+(E^3)*x2+4*(E^2)*x1+4*(E^2)*x2+2*(E^2)*x3+(E^2)*x4+3*E*x1+3*E*x2+4*E*x3+3*E*x4
[junit] upperBound2 = 2*(E^3)*M+11*(E^2)*M+13*E*M
[junit] = 2*(E^2+11/2*E+13/2)*E*M
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.HerbrandTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] test12: a = PLUS_REAL(1h,2h)
[junit] test12: b = PLUS_REAL(2h,1h)
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.MixedArithmeticTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] herbrandSimplify: e1 = PLUS_INT(X,1h)
[junit] herbrandSimplify: p = 0 == -1*(int)X+2
[junit] herbrandSimplify: e2 = PLUS_INT(2h,1h)
[junit] test12herbrand: a = PLUS_REAL(1h,2h)
[junit] test12herbrand: b = PLUS_REAL(2h,1h)
[junit] test12ideal: a = 3
[junit] test12ideal: b = 3
[junit] hrelations: assumption : LTE_INT(1h,X) && LTE_INT(X,1h)
[junit] hrelations: newAssumption : LTE_INT(1h,X) && LTE_INT(X,1h)
[junit] herbrandSame: a = TIMES_REAL(1h,2h)
[junit] herbrandSame: b = TIMES_REAL(1h,2h)
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.ReferenceTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.022 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] identity: identityReference = (Ref<int>)<1>
[junit] identity: a1 = (real[3])<1,2,3>
[junit] identity: a2 = a2
[junit] identity: t1 = (tuple<CHAR,real>)<'c',3>
[junit] identity: t2 = t2
[junit] arrayElement: ar0 = ArrayElementRef((Ref<int>)<1>,0)
[junit] arrayElement: ar1 = ArrayElementRef((Ref<int>)<1>,1)
[junit] arrayElement: ar2 = ArrayElementRef((Ref<int>)<1>,2)
[junit] arrayElement: ari = ArrayElementRef((Ref<int>)<1>,i)
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.TupleTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] tuple1: tuple = (tup<int,int>)<1,2>
[junit] tuple1: tuple = (tup<int,int>)<3,2>
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.UnionTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.012 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] a[0:=inject(1,2/3), 1:=inject(2,true), 2:=inject(0,10)]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.IF.malsulmiTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 3, Time elapsed: 0.011 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] X = -2
[junit] Y = -1
[junit] ------------- ---------------- ---------------
[junit] Testcase: test1(edu.udel.cis.vsl.sarl.IF.malsulmiTest):SKIPPED
[junit] Testcase: test2(edu.udel.cis.vsl.sarl.IF.malsulmiTest):SKIPPED
[junit] Testcase: test3(edu.udel.cis.vsl.sarl.IF.malsulmiTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.CollectionsTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.IF.CollectionTest
[junit] Tests run: 0, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.012 sec
[junit]
[junit] Testcase: edu.udel.cis.vsl.sarl.collections.IF.CollectionTest: Caused an ERROR
[junit] null
[junit] java.lang.NullPointerException
[junit] at edu.udel.cis.vsl.sarl.collections.IF.CollectionTest.setUpBeforeClass(CollectionTest.java:46)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.collections.IF.CollectionTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.BasicCollectionTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.008 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.CljSortedSymbolicMapTest
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.017 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.CollectionComparatorTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.PcollectionsSymbolicMapTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.015 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.PcollectionsSymbolicSequenceTest
[junit] Tests run: 13, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.04 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.PcollectionsSymbolicSetTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.013 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.collections.common.commonCollectionFactoryTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.expr.ExpressionTest
[junit] Tests run: 41, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 0.073 sec
[junit]
[junit] Testcase: standardSimplifierFactory(edu.udel.cis.vsl.sarl.expr.ExpressionTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest
[junit] Tests run: 11, Failures: 1, Errors: 2, Skipped: 0, Time elapsed: 0.015 sec
[junit]
[junit] Testcase: forallTest(edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest): Caused an ERROR
[junit] null
[junit] java.lang.NullPointerException
[junit] at edu.udel.cis.vsl.sarl.expr.common.CommonSymbolicExpression.computeHashCode(CommonSymbolicExpression.java:162)
[junit] at edu.udel.cis.vsl.sarl.object.common.CommonSymbolicObject.hashCode(CommonSymbolicObject.java:112)
[junit] at org.pcollections.HashPMap.containsKey(HashPMap.java:84)
[junit] at org.pcollections.MapPSet.contains(MapPSet.java:69)
[junit] at org.pcollections.MapPSet.plus(MapPSet.java:76)
[junit] at org.pcollections.MapPSet.plus(MapPSet.java:20)
[junit] at edu.udel.cis.vsl.sarl.collections.common.PcollectionsSymbolicSet.add(PcollectionsSymbolicSet.java:113)
[junit] at edu.udel.cis.vsl.sarl.collections.common.CommonCollectionFactory.singletonHashSet(CommonCollectionFactory.java:103)
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactory.hashSet(CnfFactory.java:67)
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactory.and(CnfFactory.java:154)
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest.forallTest(CnfFactoryTest.java:169)
[junit]
[junit]
[junit] Testcase: orTest(edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest): FAILED
[junit] expected:<false> but was:<(!p) && p>
[junit] junit.framework.AssertionFailedError: expected:<false> but was:<(!p) && p>
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest.orTest(CnfFactoryTest.java:235)
[junit]
[junit]
[junit] Testcase: existsTest2(edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest): Caused an ERROR
[junit] null
[junit] java.lang.NullPointerException
[junit] at edu.udel.cis.vsl.sarl.expr.common.CommonSymbolicExpression.computeHashCode(CommonSymbolicExpression.java:162)
[junit] at edu.udel.cis.vsl.sarl.object.common.CommonSymbolicObject.hashCode(CommonSymbolicObject.java:112)
[junit] at org.pcollections.HashPMap.containsKey(HashPMap.java:84)
[junit] at org.pcollections.MapPSet.contains(MapPSet.java:69)
[junit] at org.pcollections.MapPSet.plus(MapPSet.java:76)
[junit] at org.pcollections.MapPSet.plus(MapPSet.java:20)
[junit] at edu.udel.cis.vsl.sarl.collections.common.PcollectionsSymbolicSet.add(PcollectionsSymbolicSet.java:113)
[junit] at edu.udel.cis.vsl.sarl.collections.common.CommonCollectionFactory.singletonHashSet(CommonCollectionFactory.java:103)
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactory.hashSet(CnfFactory.java:67)
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactory.or(CnfFactory.java:235)
[junit] at edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest.existsTest2(CnfFactoryTest.java:367)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.expr.cnf.CnfFactoryTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealAddTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.015 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealBooleanTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealDivideTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.016 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] b1=10
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealEqualityTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.01 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] Equals=0 == -2*Y
[junit] neq=false
[junit] neq1=true
[junit] neq2=0 != -2*Y
[junit] b1=X/Y <= 0
[junit] b2=0 < X/Y
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealModulusTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] modulo=0
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealMultiplyTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.007 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] constantMultiply: 3/2 * -1/4 = -3/8
[junit] xp1xm1=X^2+-1
[junit] x2m1=X^2+-1
[junit] Multiply_Polynomial=2*(X^4)+3*(X^2)+1
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealPowerTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 0.004 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] xplus1squared: X^2+2*X+1 vs. X^2+2*X+1
[junit] ------------- ---------------- ---------------
[junit] Testcase: bigPower(edu.udel.cis.vsl.sarl.ideal.IdealPowerTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealSubtractTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] Constant Term Subtraction1=10*(X^2)+10*X
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.IdealTypeTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.01 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] Zero Polynomial=0
[junit] Number=3
[junit] constantCreation: 10
[junit] symbolicConstantCreate: X
[junit] n22=-1*(real)X+-10
[junit] ADD=8
[junit] MULTIPLY=15
[junit] MINUS=-5
[junit] POWER=5^3
[junit] POWER0=125
[junit] SUBTRACT=2
[junit] COND=X ? true : true
[junit] CAST=int
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.AffineExpressionTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.014 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] 6*0+6
[junit] 2020708769
[junit] Epic fail!:null
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.AffineFactoryTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectCloneTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectConstantTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.012 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectEqualsTest
[junit] Tests run: 11, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.012 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectIsConsistentTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.01 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectIsRealTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectMakeConstantTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 0.012 sec
[junit]
[junit] Testcase: makeConstantIntRatTest(edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectMakeConstantTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectNewLowerTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectNewUpperTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectRestrictLowerTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.012 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectRestrictUpperTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectSetLowerTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.013 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.BoundsObjectSetUpperTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.DividesTest
[junit] Tests run: 2, Failures: 2, Errors: 0, Skipped: 0, Time elapsed: 0.008 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] x : int : 1
[junit] apply: x
[junit] ------------- ---------------- ---------------
[junit] Testcase: dividBenchTest(edu.udel.cis.vsl.sarl.ideal.simplify.DividesTest): FAILED
[junit] expected:<true> but was:<0 == -1*(y%x)>
[junit] junit.framework.AssertionFailedError: expected:<true> but was:<0 == -1*(y%x)>
[junit] at edu.udel.cis.vsl.sarl.ideal.simplify.DividesTest.dividBenchTest(DividesTest.java:219)
[junit]
[junit]
[junit] Testcase: test1(edu.udel.cis.vsl.sarl.ideal.simplify.DividesTest): FAILED
[junit] expected:<z> but was:<0 == -1*(x%y)>
[junit] junit.framework.AssertionFailedError: expected:<z> but was:<0 == -1*(x%y)>
[junit] at edu.udel.cis.vsl.sarl.ideal.simplify.DividesTest.test1(DividesTest.java:135)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.ideal.simplify.DividesTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierBBTest
[junit] Tests run: 4, Failures: 2, Errors: 0, Skipped: 0, Time elapsed: 0.027 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] here: 0 == -1*(x^4)
[junit] 0 == -1*(x^4)
[junit] ------------- ---------------- ---------------
[junit] Testcase: singlePowerTermSimplifyTest(edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierBBTest): FAILED
[junit] Values should be different. Actual: 0 == -1*(x^4)
[junit] junit.framework.AssertionFailedError: Values should be different. Actual: 0 == -1*(x^4)
[junit] at edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierBBTest.singlePowerTermSimplifyTest(IdealSimplifierBBTest.java:115)
[junit]
[junit]
[junit] Testcase: twoStagePolyTest(edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierBBTest): FAILED
[junit] expected:<0> but was:<0^3>
[junit] junit.framework.AssertionFailedError: expected:<0> but was:<0^3>
[junit] at edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierBBTest.twoStagePolyTest(IdealSimplifierBBTest.java:85)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierBBTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierSimpExprTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.04 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] 25*(x^4)*(y^3)
[junit] -300*(x^2)
[junit] 20*(x^4)*(y^3)
[junit] 200*(x^2)
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.IdealSimplifierTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.026 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.LinearSolverTest
[junit] Tests run: 1, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testcase: initializationError(edu.udel.cis.vsl.sarl.ideal.simplify.LinearSolverTest): Caused an ERROR
[junit] No runnable methods
[junit] java.lang.Exception: No runnable methods
[junit] at java.lang.reflect.Constructor.newInstance(Constructor.java:525)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.ideal.simplify.LinearSolverTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.SimpBoolTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.01 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.SimplifierIntervalTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.SimplifyEqualsZeroTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.008 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.ideal.simplify.SimplifyFPTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.008 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] xInt^2+-1
[junit] xInt^2+1
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.numbers.ExponentiatorTest
[junit] Tests run: 1, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testcase: compareResults(edu.udel.cis.vsl.sarl.numbers.ExponentiatorTest): Caused an ERROR
[junit] null
[junit] java.lang.NullPointerException
[junit] at edu.udel.cis.vsl.sarl.numbers.ExponentiatorTest.compareResults(ExponentiatorTest.java:38)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.numbers.ExponentiatorTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.numbers.NumberFactoryTest
[junit] Tests run: 61, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.024 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.numbers.RealNumberTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.ObjectsTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.CommonBooleanObjectTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.CommonCharObjectTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.CommonIntObjectTest
[junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.007 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.CommonNumberObjectTest
[junit] Tests run: 14, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.007 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.CommonObjectFactoryTest
[junit] Tests run: 26, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.CommonStringObjectTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.object.common.ObjectComparatorTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.006 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.IF.ObjectWithIdTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] [true, false, 0, 1, 0, 0, 1, 1, boolean, int, hint, real, hreal, CHAR, {}, {}, true, false, 1, 1, 0, 0, NULL, <0>, <1>, Ref, Ref<int>, <Ref<int>,int>->Ref<int>, ArrayElementRef, ArrayElementRef, TupleComponentRef, TupleComponentRef, UnionMemberRef, UnionMemberRef, OffsetRef, OffsetRef, (Ref<int>)<0>, (Ref<int>)<1>, {}, <>, Hello]------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.ArrayTest
[junit] Tests run: 41, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.028 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.BoundCleanerTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.004 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] forall x : real . (0 < -1*x+1)
[junit] forall x'1 : real . (0 < x'1)
[junit] (forall x'2 : real . (0 < x'2)) && (forall x'3 : real . (0 < -1*x'3+1))
[junit] (forall x'1 : real . (exists x : real . (0 < x))) && (forall x'2 : real . (0 < -1*x'2+1))
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest
[junit] Tests run: 57, Failures: 0, Errors: 1, Skipped: 9, Time elapsed: 0.032 sec
[junit]
[junit] Testcase: testIdentityReference(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testSubstituteSymbolicExpressionSymbolicConstantSymbolicExpression(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testTupleComponentReference(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testUnionTypeStringObjectIterableOfQextendsSymbolicType(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testUnionMemberReference(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testArrayLambda(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest): Caused an ERROR
[junit] Argument arrayType to method arrayLambda was null
[junit] edu.udel.cis.vsl.sarl.IF.SARLException: Argument arrayType to method arrayLambda was null
[junit] at edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.err(CommonPreUniverse.java:214)
[junit] at edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.arrayLambda(CommonPreUniverse.java:1953)
[junit] at edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest.testArrayLambda(CommonPreUniverseTest.java:676)
[junit]
[junit]
[junit] Testcase: testIntegerBigInteger(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testOffsetReference(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testDereference(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] Testcase: testArrayElementReference(edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest):SKIPPED
[junit] TEST edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverseTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.ExpressionSubstituteTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.FunctionCaseEqualsTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 0.003 sec
[junit]
[junit] Testcase: symbolicEqualsTest(edu.udel.cis.vsl.sarl.preuniverse.common.FunctionCaseEqualsTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.FunctionTypeTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.MakeTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.OptimizedMapTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.004 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] 0------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.PureTypeTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.TupleTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.TypeTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.preuniverse.common.UnionTest
[junit] Tests run: 14, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.013 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] a[0:=inject(1,2/3), 1:=inject(2,true), 2:=inject(0,10)]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.ProveTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.004 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest
[junit] Tests run: 16, Failures: 0, Errors: 3, Skipped: 0, Time elapsed: 0.048 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] key = Expr[FALSE, type=BOOLEAN, kind=_FALSE_EXPR]
[junit] value = Expr[FALSE, type=BOOLEAN, kind=_FALSE_EXPR]
[junit] ------------- ---------------- ---------------
[junit] Testcase: isApplyExpr(edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest): Caused an ERROR
[junit] A SARL internal error has occurred.
[junit] Please send an error report to siegel@udel.edu.
[junit] Unknown CVC3 variable: var
[junit] edu.udel.cis.vsl.sarl.IF.SARLInternalException: A SARL internal error has occurred.
[junit] Please send an error report to siegel@udel.edu.
[junit] Unknown CVC3 variable: var
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.typeOf(CVC3ModelFinder.java:287)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.computeModel(CVC3ModelFinder.java:785)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.<init>(CVC3ModelFinder.java:99)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest.isApplyExpr(CVC3ModelFinderTest.java:248)
[junit]
[junit]
[junit] Testcase: AssignArrayRealType(edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest): Caused an ERROR
[junit] A SARL internal error has occurred.
[junit] Please send an error report to siegel@udel.edu.
[junit] Unable to back translate: (a).1[0]
[junit] edu.udel.cis.vsl.sarl.IF.SARLInternalException: A SARL internal error has occurred.
[junit] Please send an error report to siegel@udel.edu.
[junit] Unable to back translate: (a).1[0]
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.backTranslateArrayLiteral(CVC3ModelFinder.java:389)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.backTranslateTuple(CVC3ModelFinder.java:434)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.backTranslate(CVC3ModelFinder.java:474)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.computeModel(CVC3ModelFinder.java:785)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.<init>(CVC3ModelFinder.java:99)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3TheoremProver.validOrModel(CVC3TheoremProver.java:1608)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest.AssignArrayRealType(CVC3ModelFinderTest.java:498)
[junit]
[junit]
[junit] Testcase: assignApplyElseStatement(edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest): Caused an ERROR
[junit] A SARL internal error has occurred.
[junit] Please send an error report to siegel@udel.edu.
[junit] Unable to back translate: (a).1[0]
[junit] edu.udel.cis.vsl.sarl.IF.SARLInternalException: A SARL internal error has occurred.
[junit] Please send an error report to siegel@udel.edu.
[junit] Unable to back translate: (a).1[0]
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.backTranslateArrayLiteral(CVC3ModelFinder.java:389)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.backTranslateTuple(CVC3ModelFinder.java:434)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.backTranslate(CVC3ModelFinder.java:474)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.computeModel(CVC3ModelFinder.java:785)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinder.<init>(CVC3ModelFinder.java:99)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3TheoremProver.validOrModel(CVC3TheoremProver.java:1608)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest.assignApplyElseStatement(CVC3ModelFinderTest.java:478)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.prove.cvc.CVC3ModelFinderTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3ProcessEqualityTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.013 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3SideEffectTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TheoremProverTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 0.006 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit]
[junit] SARL context 0: true
[junit] SARL predicate 0: true
[junit]
[junit] CVC3 assumptions 0: TRUE
[junit] CVC3 predicate 0: TRUE
[junit] CVC3 result 0: VALID
[junit]
[junit] SARL context 0: true
[junit] SARL predicate 0: false
[junit]
[junit] CVC3 assumptions 0: TRUE
[junit] CVC3 predicate 0: FALSE
[junit] CVC3 result 0: INVALID
[junit] {true=TRUE, false=FALSE}
[junit] ------------- ---------------- ---------------
[junit] Testcase: testNewCVCName(edu.udel.cis.vsl.sarl.prove.cvc.CVC3TheoremProverTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateAddTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateAndTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.006 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateDivisionTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateFunctionTest
[junit] Tests run: 3, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.049 sec
[junit]
[junit] Testcase: testTranslateFunctionLambda(edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateFunctionTest): Caused an ERROR
[junit] Parse Error: cannot resolve an identifier: "f"
[junit] cvc3.ParserException: Parse Error: cannot resolve an identifier: "f"
[junit] at cvc3.ValidityChecker.jniExprFromString(Native Method)
[junit] at cvc3.ValidityChecker.exprFromString(ValidityChecker.java:834)
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateFunctionTest.testTranslateFunctionLambda(CVC3TranslateFunctionTest.java:135)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateFunctionTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateMathTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.008 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateNegativeTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.004 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateOrTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslatePowerTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.004 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateQuantifierTest
[junit] Tests run: 4, Failures: 2, Errors: 0, Skipped: 0, Time elapsed: 0.007 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] Expected: ((EXISTS (x'1: REAL) : (0 < x)) AND (EXISTS (x'1: REAL) : (x < 10)))
[junit] Result: ((EXISTS (x'1: REAL) : (0 < x)) AND (EXISTS (x'1: REAL) : (x < 10)))
[junit] Should be: ((EXISTS (x: REAL) : (0 < x)) AND (EXISTS (x'1: REAL) : (x'1 < 10)))
[junit]
[junit] Result: ((EXISTS (x: INT) : (x'1 < 0)) AND (EXISTS (x'1: INT) : (0 < x'1)) AND (EXISTS (x'1: INT) : (x'1 < 10)))
[junit] Should be: ((EXISTS (x: INT) : (0 < x)) AND (EXISTS (x'1: INT) : (x'1 < 10)) AND (EXISTS (x'2: INT) : (x'2 < 0)))
[junit] expected: (FORALL (values'1: [INT, (ARRAY INT OF INT)]) : (0 < values'1))
[junit] translateResult: (FORALL (values: [INT, (ARRAY INT OF INT)]) : (0 < values'1))
[junit]
[junit] ------------- ---------------- ---------------
[junit] Testcase: testForAll(edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateQuantifierTest): FAILED
[junit] expected:<(FORALL (values'1: [INT, (ARRAY INT OF INT)]) : (0 < values'1))> but was:<(FORALL (values: [INT, (ARRAY INT OF INT)]) : (0 < values'1))>
[junit] junit.framework.AssertionFailedError: expected:<(FORALL (values'1: [INT, (ARRAY INT OF INT)]) : (0 < values'1))> but was:<(FORALL (values: [INT, (ARRAY INT OF INT)]) : (0 < values'1))>
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateQuantifierTest.testForAll(CVC3TranslateQuantifierTest.java:290)
[junit]
[junit]
[junit] Testcase: testTranslateExists(edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateQuantifierTest): FAILED
[junit] expected:<(EXISTS (x: REAL) : ((0 < x) AND (x < N)))> but was:<(EXISTS (x'1: REAL) : ((0 < x) AND (x < N)))>
[junit] junit.framework.AssertionFailedError: expected:<(EXISTS (x: REAL) : ((0 < x) AND (x < N)))> but was:<(EXISTS (x'1: REAL) : ((0 < x) AND (x < N)))>
[junit] at edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateQuantifierTest.testTranslateExists(CVC3TranslateQuantifierTest.java:123)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateQuantifierTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateReadWriteArrayTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.011 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateReadWriteTupleTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateSubtractTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.009 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3TranslateTypeTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.007 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] expected: [INT, (ARRAY INT OF INT)]
[junit] translateResult: [INT, (ARRAY INT OF INT)]
[junit]
[junit] expected: [INT, INT, REAL]
[junit] translateResult: [INT, INT, REAL]
[junit]
[junit] translateResult: union
[junit]
[junit] expected: INT -> INT
[junit] translateResult: INT -> INT
[junit]
[junit] expected: (INT, INT) -> BOOLEAN
[junit] translateResult: (INT, INT) -> BOOLEAN
[junit]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.prove.cvc.CVC3UnionTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.simplify.SimplifyArrayTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] NTPolynomial[ADD; real; {SortedMap{a[1]->a[1], a[2]->a[2], a[0]->a[0]}}]
[junit] NTPolynomial[ADD; real; {SortedMap{a[1]->a[1], a[2]->a[2], a[0]->a[0]}}]
[junit] NTPolynomial[ADD; real; {SortedMap{a[1]->a[1], a[2]->a[2], a[0]->a[0]}}]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.simplify.SimplifyCreationTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.004 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.TypesTest
[junit] Tests run: 1, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testcase: initializationError(edu.udel.cis.vsl.sarl.type.TypesTest): Caused an ERROR
[junit] No runnable methods
[junit] java.lang.Exception: No runnable methods
[junit] at java.lang.reflect.Constructor.newInstance(Constructor.java:525)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.type.TypesTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayTypeTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayTypeTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicFunctionTypeTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicIntegerTypeTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicPrimitiveTypeTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicRealTypeTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTupleTypeTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest
[junit] Tests run: 19, Failures: 19, Errors: 0, Skipped: 0, Time elapsed: 0.046 sec
[junit]
[junit] Testcase: testArrayType2(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testPureType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testHerbrandIntegerType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testTupleType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testArrayType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testsingletonSequence(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testSequence2(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testRealType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testUnionType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testCharacterType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testIntegerType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testSetExpressionComparator(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testTypeSequenceComparator(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testTypeComparator(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testFunctionType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testHerbrandRealType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testObjectFactory(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testBooleanType(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] Testcase: testSequence(edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicArrayType.<init>(CommonSymbolicArrayType.java:47)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicCompleteArrayType.<init>(CommonSymbolicCompleteArrayType.java:33)
[junit] at edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest.setUp(CommonSymbolicTypeFactoryTest.java:140)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeFactoryTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeSequenceTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicTypeTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.001 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.CommonSymbolicUnionTypeTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.TypeComparatorTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.type.common.TypeSequenceComparatorTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.001 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.sarl.universe.IdealSimplifyTest
[junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.037 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] Path condition is unsatisfiable.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.sarl.universe.IdealUniverseTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.005 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] x = X
[junit] y = Y
[junit] two = 2
[junit] three = 3
[junit]
[junit] subExpression: expr = (tup<int,real>[3])<(tup<int,real>)<1,157/50>,(tup<int,real>)<1,157/50>,(tup<int,real>)<-2,1359/500>>
[junit] subExpression: map = {(tup<int,real>)<1,157/50>=(tup<int,real>)<-2,1359/500>}
[junit] subExpression: expected = (tup<int,real>[3])<(tup<int,real>)<-2,1359/500>,(tup<int,real>)<-2,1359/500>,(tup<int,real>)<-2,1359/500>>
[junit] x = X
[junit] y = Y
[junit] two = 2
[junit] three = 3
[junit]
[junit] subArray1: array1 = a[0:=x0, 1:=x1, 2:=x2]
[junit] subArray1: array2 = a[0:=x2, 1:=x1, 2:=x0]
[junit] x = X
[junit] y = Y
[junit] two = 2
[junit] three = 3
[junit]
[junit] sub1: u = X+2*Y
[junit] sub1: map = {X=Y}
[junit] sub1: newU = 3*Y
[junit] x = X
[junit] y = Y
[junit] two = 2
[junit] three = 3
[junit]
[junit] sub2: u = X+2*Y
[junit] sub2: map = {X=Y, Y=X}
[junit] sub2: newU = 2*X+Y
[junit] ------------- ---------------- ---------------
[junitreport] Processing /Users/tester/work/sarl/mile2/r1162/junit/data/TESTS-TestSuites.xml to /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null546264802
[junitreport] Loading stylesheet jar:file:/opt/local/share/java/apache-ant/lib/ant-junit.jar!/org/apache/tools/ant/taskdefs/optional/junit/xsl/junit-frames.xsl
[junitreport] Transform time: 1113ms
[junitreport] Deleting: /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null546264802
test:
[jacoco:report] Loading execution data file /Users/tester/work/sarl/mile2/r1162/jacoco.exec
[jacoco:report] Writing group "Test Coverage Report for SARL mile2 r1162" with 159 classes
javadoc:
[mkdir] Created dir: /Users/tester/work/sarl/mile2/r1162/doc/javadoc
[javadoc] Generating Javadoc
[javadoc] Javadoc execution
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.IF.expr...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.IF.number...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.IF.object...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.IF.type...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.collections...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.collections.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.collections.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.expr...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.expr.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.expr.cnf...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.expr.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.herbrand...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.herbrand.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.ideal...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.ideal.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.ideal.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.ideal.simplify...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.number...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.number.real...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.object...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.object.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.object.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.preuniverse...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.preuniverse.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.preuniverse.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.prove...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.prove.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.prove.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.prove.cvc...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.reason...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.reason.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.reason.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.simplify...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.simplify.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.simplify.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.type...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.type.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.type.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.universe...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.universe.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.sarl.util...
[javadoc] Constructing Javadoc information...
[javadoc] Standard Doclet version 1.7.0_15
[javadoc] Building tree for all the packages and classes...
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/IF/NumericExpressionFactory.java:194: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/IF/NumericExpressionFactory.java:201: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/IF/NumericExpressionFactory.java:208: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/IF/NumericExpressionFactory.java:215: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/common/CommonArrayElementReference.java:48: warning - Tag @return cannot be used in constructor documentation. It can only be used in the following types of documentation: method.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/common/CommonArrayElementReference.java:48: warning - Parameter "parentIndexSequence" is documented more than once.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/common/CommonArrayElementReference.java:79: warning - @retrun is an unknown tag.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/common/CommonExpressionFactory.java:105: warning - Tag @return cannot be used in constructor documentation. It can only be used in the following types of documentation: method.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/common/CommonNumericExpressionFactory.java:83: warning - Tag @return cannot be used in constructor documentation. It can only be used in the following types of documentation: method.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/expr/common/CommonOffsetReference.java:45: warning - Tag @return cannot be used in constructor documentation. It can only be used in the following types of documentation: method.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:77: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:108: warning - Parameter "type" is documented more than once.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:121: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:134: warning - Parameter "type" is documented more than once.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:149: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:163: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:190: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:203: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/IF/IdealFactory.java:217: warning - @param argument "type" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/ideal/simplify/BoundsObject.java:349: warning - @return tag cannot be used in method with void return type.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/number/real/Exponentiator.java:70: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/number/real/RealNumberFactory.java:164: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/preuniverse/IF/PreUniverse.java:615: warning - @param argument "char" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/preuniverse/IF/PreUniverse.java:622: warning - @param argument "String" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/preuniverse/IF/PreUniverse.java:727: warning - @param argument "arg0" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/preuniverse/IF/PreUniverse.java:727: warning - @param argument "arg1" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/preuniverse/IF/PreUniverse.java:1386: warning - @param argument "SymbolicType" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/prove/cvc/CVC3ModelFinder.java:202: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/prove/cvc/CVC3ModelFinder.java:214: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/prove/cvc/CVC3ModelFinder.java:549: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/prove/cvc/CVC3TheoremProver.java:806: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/prove/cvc/CVC3TheoremProver.java:1100: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/prove/cvc/CVC3TheoremProver.java:1570: warning - @param argument "expr" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/type/common/CommonSymbolicTypeSequence.java:59: warning - @param argument "types:" is not a parameter name.
[javadoc] /Users/tester/work/sarl/mile2/r1162/src/edu/udel/cis/vsl/sarl/type/common/CommonSymbolicTypeSequence.java:75: warning - @param argument "types:" is not a parameter name.
[javadoc] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Generating /Users/tester/work/sarl/mile2/r1162/doc/javadoc/help-doc.html...
[javadoc] 35 warnings
[javadoc] Patched 1 link injection vulnerable javadocs
all:
BUILD SUCCESSFUL
Total time: 17 seconds
Stderr:
[junit] Tests FAILED