| Test |
Method name |
Duration |
Result |
| [10]
; Problem: New line before ')'
( a b c d
)
,
; Problem: New line before ')'
(a b c d)
|
testIdemPotent(String, String)[10] |
0.001s |
passed |
| [11]
; From a bug:
(assert(not
; The formula to be proved:
(=> (and (and (= 6 a_2 ) (= 3 b_3 ) ) (= 2 c_4 ) ) (= c_4 (div a_2 b_3 ) ) )
)) ; End of assert.
(check-sat)
; end of smt problem declaration,
; From a bug:
(assert
(not
; The formula to be proved:
(=> (and (and (= 6 a_2) (= 3 b_3)) (= 2 c_4)) (= c_4 (div a_2 b_3)))))
; End of assert.
(check-sat)
; end of smt problem declaration |
testIdemPotent(String, String)[11] |
0.001s |
passed |
| [1]
(declare-fun f (Int) Int)
, (declare-fun f (Int) Int)
|
testIdemPotent(String, String)[1] |
0s |
passed |
| [2]
(assert (forall ((x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)) (> x 0)))
,
(assert
(forall
((x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int))
(> x 0)))
|
testIdemPotent(String, String)[2] |
0.001s |
passed |
| [3]
(assert (forall (! ((x Int)) (=> longName________________ (> x 0)) :pattern ((+ 2 x)))))
,
(assert
(forall
(! ((x Int)) (=> longName________________ (> x 0)) :pattern ((+ 2 x)))))
|
testIdemPotent(String, String)[3] |
0s |
passed |
| [4]
(assert |long name with spaces is not broken when longer than 80 characters even this is a ridiculously long name|)
,
(assert
|long name with spaces is not broken when longer than 80 characters even this is a ridiculously long name|)
|
testIdemPotent(String, String)[4] |
0s |
passed |
| [5]
(and true true true true true true true true true true true true true true true
true true true true true true true true true true true true true true true)
,
(and
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true)
|
testIdemPotent(String, String)[5] |
0.001s |
passed |
| [6]
; Now only comments
; but multiple rows of them!
; with indentations (which are lost)
; and long lines too xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx xxxxxxxxxxxxxxxx xxxxxxxxxxX
,
; Now only comments
; but multiple rows of them!
; with indentations (which are lost)
; and long lines too xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx xxxxxxxxxxxxxxxx xxxxxxxxxxX
|
testIdemPotent(String, String)[6] |
0.001s |
passed |
| [7]
(assert (and looooooooooooooooooooooooooooooooooooooooooooong short ; false false commented out
after))
,
(assert
(and
looooooooooooooooooooooooooooooooooooooooooooong
short
; false false commented out
after))
|
testIdemPotent(String, String)[7] |
0s |
passed |
| [8]
(assert (f x ; inline comments break lines
(after 42)))
,
(assert
(f
x
; inline comments break lines
(after 42)))
|
testIdemPotent(String, String)[8] |
0s |
passed |
| [9]
(assert (last is comment) ; end of smt problem declaration
)
,
(assert
(last is comment)
; end of smt problem declaration
)
|
testIdemPotent(String, String)[9] |
0.001s |
passed |
| [10]
; Problem: New line before ')'
( a b c d
)
,
; Problem: New line before ')'
(a b c d)
|
testSMTBeautifier(String, String)[10] |
0.001s |
passed |
| [11]
; From a bug:
(assert(not
; The formula to be proved:
(=> (and (and (= 6 a_2 ) (= 3 b_3 ) ) (= 2 c_4 ) ) (= c_4 (div a_2 b_3 ) ) )
)) ; End of assert.
(check-sat)
; end of smt problem declaration,
; From a bug:
(assert
(not
; The formula to be proved:
(=> (and (and (= 6 a_2) (= 3 b_3)) (= 2 c_4)) (= c_4 (div a_2 b_3)))))
; End of assert.
(check-sat)
; end of smt problem declaration |
testSMTBeautifier(String, String)[11] |
0s |
passed |
| [1]
(declare-fun f (Int) Int)
, (declare-fun f (Int) Int)
|
testSMTBeautifier(String, String)[1] |
0.002s |
passed |
| [2]
(assert (forall ((x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)(x Int)) (> x 0)))
,
(assert
(forall
((x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int)
(x Int))
(> x 0)))
|
testSMTBeautifier(String, String)[2] |
0s |
passed |
| [3]
(assert (forall (! ((x Int)) (=> longName________________ (> x 0)) :pattern ((+ 2 x)))))
,
(assert
(forall
(! ((x Int)) (=> longName________________ (> x 0)) :pattern ((+ 2 x)))))
|
testSMTBeautifier(String, String)[3] |
0.005s |
passed |
| [4]
(assert |long name with spaces is not broken when longer than 80 characters even this is a ridiculously long name|)
,
(assert
|long name with spaces is not broken when longer than 80 characters even this is a ridiculously long name|)
|
testSMTBeautifier(String, String)[4] |
0.001s |
passed |
| [5]
(and true true true true true true true true true true true true true true true
true true true true true true true true true true true true true true true)
,
(and
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true
true)
|
testSMTBeautifier(String, String)[5] |
0.001s |
passed |
| [6]
; Now only comments
; but multiple rows of them!
; with indentations (which are lost)
; and long lines too xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx xxxxxxxxxxxxxxxx xxxxxxxxxxX
,
; Now only comments
; but multiple rows of them!
; with indentations (which are lost)
; and long lines too xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx xxxxxxxxxxxxxxxx xxxxxxxxxxX
|
testSMTBeautifier(String, String)[6] |
0.001s |
passed |
| [7]
(assert (and looooooooooooooooooooooooooooooooooooooooooooong short ; false false commented out
after))
,
(assert
(and
looooooooooooooooooooooooooooooooooooooooooooong
short
; false false commented out
after))
|
testSMTBeautifier(String, String)[7] |
0s |
passed |
| [8]
(assert (f x ; inline comments break lines
(after 42)))
,
(assert
(f
x
; inline comments break lines
(after 42)))
|
testSMTBeautifier(String, String)[8] |
0s |
passed |
| [9]
(assert (last is comment) ; end of smt problem declaration
)
,
(assert
(last is comment)
; end of smt problem declaration
)
|
testSMTBeautifier(String, String)[9] |
0s |
passed |