horn-smt-pos-el
numeric-sort-03.smt2.horn.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: numeric-sort-03.smt2.horn.smt2.horn.smt2:16:29-16:29: Error numeric-sort-03.smt2.horn.smt2.horn.smt2:16:29: | 16 | (forall ((cond (obj bool)) ((<=> cond (<= n zero)))) | ^^^^^^^ unexpected "obj boo" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/numeric-sort-03.smt2.horn.smt2.horn.smt2/' to rerun this test only.
numeric-sort-03.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/numeric-sort-03.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/numeric-sort-03.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 8292: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.04s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '$0=="Tests.Unit.horn-smt-pos-el.numeric-sort-03.smt2.horn.smt2"' to rerun this test only.
test00.smt2.horn.smt2: OK (0.03s)
test01.smt2.horn.smt2: OK (0.03s)
numeric-sort-02.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/numeric-sort-02.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/numeric-sort-02.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 8292: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.03s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '/numeric-sort-02.smt2.horn.smt2/' to rerun this test only.
ple_sum_fuel.4.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_sum_fuel.4.smt2.horn.smt2:8:16-8:16: Error ple_sum_fuel.4.smt2.horn.smt2:8:16: | 8 | (constant sum ((func 0 (Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/ple_sum_fuel.4.smt2.horn.smt2/' to rerun this test only.
icfp17-ex1.smt2.horn.smt2: OK (0.03s)
scrape01.smt2.horn.smt2: OK (0.04s)
icfp17-ex3.smt2.horn.smt2: OK (0.03s)
test00.smt2.horn.smt2.horn.smt2: OK (0.03s)
ple_list00.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_list00.smt2.horn.smt2:6:16-6:16: Error ple_list00.smt2.horn.smt2:6:16: | 6 | (constant len ((func 1 ((MyList @(0))) Int))) | ^^^^^^^ unexpected "(func 1" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/horn-smt-pos-el.ple_list00.smt2.horn.smt2/' to rerun this test only.
numeric-sort-00.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/numeric-sort-00.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/numeric-sort-00.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 8095: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.03s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '/horn-smt-pos-el.numeric-sort-00.smt2.horn.smt2/' to rerun this test only.
test03.smt2.horn.smt2: OK (0.03s)
test02.smt2.horn.smt2: OK (0.03s)
numeric-sort-01.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/numeric-sort-01.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/numeric-sort-01.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 8095: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.03s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '/numeric-sort-01.smt2.horn.smt2/' to rerun this test only.
maps00.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: maps00.smt2.horn.smt2:12:43-12:43: Error maps00.smt2.horn.smt2:12:43: | 12 | (forall ((m1 (Map_t Int Int)) ((= m1 (Map_default 0)))) | ^^^^^^ unexpected "Map_de" expecting "!=", "!~", ".", "/.", "<=", "<=>", "=>", ">=", "ETAbs", "ETApp", "and", "cast", "coerce", "exists", "forall", "if", "lam", "mod", "not", "or", "~~", '', '+', '-', '/', '<', '=', or '>'
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/maps00.smt2.horn.smt2/' to rerun this test only.
icfp17-ex2.smt2.horn.smt2: OK (0.03s)
scrape00.smt2.horn.smt2: OK (0.04s)
ebind02.smt2.horn.smt2: OK (0.03s)
bitv.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: bitv.smt2.horn.smt2:11:47-11:47: Error bitv.smt2.horn.smt2:11:47: | 11 | (forall ((one_ (BitVec Size32)) ((= one_ (int_to_bv32 1)))) | ^^^^^^ unexpected "int_to" expecting "!=", "!~", ".", "/.", "<=", "<=>", "=>", ">=", "ETAbs", "ETApp", "and", "cast", "coerce", "exists", "forall", "if", "lam", "mod", "not", "or", "~~", '', '+', '-', '/', '<', '=', or '>'
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/bitv.smt2.horn.smt2/' to rerun this test only.
ple0.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple0.smt2.horn.smt2:6:18-6:18: Error ple0.smt2.horn.smt2:6:18: | 6 | (constant adder ((func 0 (Int Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/horn-smt-pos-el.ple0.smt2.horn.smt2/' to rerun this test only.
abs02-re.smt2.horn.smt2: OK (0.03s)
ebind03.smt2.horn.smt2: OK (0.03s)
sum-rec.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/sum-rec.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/sum-rec.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 8240: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.03s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '/sum-rec.smt2.horn.smt2/' to rerun this test only.
ple_sum.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_sum.smt2.horn.smt2:7:16-7:16: Error ple_sum.smt2.horn.smt2:7:16: | 7 | (constant sum ((func 0 (Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/horn-smt-pos-el.ple_sum.smt2.horn.smt2/' to rerun this test only.
ebind01.smt2.horn.smt2: OK (0.03s)
ple_list01_adt.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_list01_adt.smt2.horn.smt2:7:16-7:16: Error ple_list01_adt.smt2.horn.smt2:7:16: | 7 | (constant len ((func 1 ((Vec @(0))) Int))) | ^^^^^^^ unexpected "(func 1" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/horn-smt-pos-el.ple_list01_adt.smt2.horn.smt2/' to rerun this test only.
constant.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: constant.smt2.horn.smt2:7:14-7:14: Error constant.smt2.horn.smt2:7:14: | 7 | (constant f ((func 0 (Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 2
Use -p '/constant.smt2.horn.smt2/' to rerun this test only.
str00.smt2.horn.smt2: OK (0.03s)
bool-neq.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/bool-neq.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/bool-neq.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 7976: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.03s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '/bool-neq.smt2.horn.smt2/' to rerun this test only.
sum-rec-ok.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Saving Horn Query: ./.liquid/sum-rec-ok.smt2.horn.smt2.horn.smt2
Saving Horn Query: ./.liquid/sum-rec-ok.smt2.horn.smt2.horn.json
Crash!: Sorry, unexpected panic in liquid-fixpoint! Error in constraint -1: crash: SMTLIB2 respSat = Error "line 3 column 8151: Sorts Int and Bool are incompatible" CRASH: -1 : ""
FAIL (0.03s)
tests/test.hs:150:
Wrong exit code
expected: ExitSuccess
but got: ExitFailure 1
Use -p '/sum-rec-ok.smt2.horn.smt2/' to rerun this test only.
horn-smt-neg-el
irregular_adt_00.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: irregular_adt_00.smt2.horn.smt2:5:16-5:16: Error irregular_adt_00.smt2.horn.smt2:5:16: | 5 | (constant len ((func 1 ((FingerTree @(0))) Int))) | ^^^^^^^ unexpected "(func 1" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/irregular_adt_00.smt2.horn.smt2/' to rerun this test only.
T523.smt2.horn.smt2: OK (0.02s)
numeric-sort-03.smt2.horn.smt2: OK (0.03s)
test00.smt2.horn.smt2: OK (0.03s)
ple_list03.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_list03.smt2.horn.smt2:6:17-6:17: Error ple_list03.smt2.horn.smt2:6:17: | 6 | (constant head ((func 1 (([] @(0))) @(0)))) | ^^^^^^^ unexpected "(func 1" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/ple_list03.smt2.horn.smt2/' to rerun this test only.
test01.smt2.horn.smt2: OK (0.04s)
ple_sum_fuel.3.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_sum_fuel.3.smt2.horn.smt2:8:16-8:16: Error ple_sum_fuel.3.smt2.horn.smt2:8:16: | 8 | (constant sum ((func 0 (Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/ple_sum_fuel.3.smt2.horn.smt2/' to rerun this test only.
ple_list00.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_list00.smt2.horn.smt2:6:16-6:16: Error ple_list00.smt2.horn.smt2:6:16: | 6 | (constant len ((func 1 ((Main.List @(0))) Int))) | ^^^^^^^ unexpected "(func 1" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/horn-smt-neg-el.ple_list00.smt2.horn.smt2/' to rerun this test only.
numeric-sort-00.smt2.horn.smt2: OK (0.03s)
test03.smt2.horn.smt2: OK (0.02s)
test02.smt2.horn.smt2: OK (0.03s)
ple0.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple0.smt2.horn.smt2:6:18-6:18: Error ple0.smt2.horn.smt2:6:18: | 6 | (constant adder ((func 0 (Int Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/horn-smt-neg-el.ple0.smt2.horn.smt2/' to rerun this test only.
abs02-re.smt2.horn.smt2: OK (0.03s)
ebind03.smt2.horn.smt2: OK (0.02s)
tag00.smt2.horn.smt2: OK (0.03s)
ple_sum.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_sum.smt2.horn.smt2:6:16-6:16: Error ple_sum.smt2.horn.smt2:6:16: | 6 | (constant sum ((func 0 (Int) Int))) | ^^^^^^^ unexpected "(func 0" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/horn-smt-neg-el.ple_sum.smt2.horn.smt2/' to rerun this test only.
ple_list01_adt.smt2.horn.smt2:
Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved.
Oops, unexpected error: ple_list01_adt.smt2.horn.smt2:6:16-6:16: Error ple_list01_adt.smt2.horn.smt2:6:16: | 6 | (constant len ((func 1 ((Vec @(0))) Int))) | ^^^^^^^ unexpected "(func 1" expecting "Int", "Integer", "Str", "bool", "func", "int", "num", "real", or uppercase letter
FAIL (0.02s)
tests/test.hs:150:
Wrong exit code
expected: ExitFailure 1
but got: ExitFailure 2
Use -p '/horn-smt-neg-el.ple_list01_adt.smt2.horn.smt2/' to rerun this test only.
liquid-fixpoint> Test suite test failed Completed 2 action(s).
Error: [S-7282] Stack failed to execute the build plan.
While executing the build plan, Stack encountered the error:
Error: [S-1995]
Test suite failure for package liquid-fixpoint-0.9.6.3
test: exited with: ExitFailure 1
Logs printed to console