mlcs-class-z3-assignment-0.1: unregistering (dependencies changed)
mlcs-class-z3-assignment> configure (lib + exe + test)
Configuring mlcs-class-z3-assignment-0.1...
mlcs-class-z3-assignment> build (lib + exe + test)
Preprocessing library for mlcs-class-z3-assignment-0.1..
Building library for mlcs-class-z3-assignment-0.1..
[1 of 4] Compiling EuropeBorders
[2 of 4] Compiling CountryColoring
[3 of 4] Compiling NQueens

/home/vyacheslav/mlcs-2021-z3-assignment-tamarinvs19/src/NQueens.hs:106:4: warning: [-Wunused-matches]
    Defined but not used: ‘one’
    |
106 |    one <- mkInt 1 sort
    |    ^^^

/home/vyacheslav/mlcs-2021-z3-assignment-tamarinvs19/src/NQueens.hs:110:11: warning: [-Wtype-defaults]
    • Defaulting the following constraints to type ‘Integer’
        (Integral a0)
          arising from a use of ‘mkIntNum’ at src/NQueens.hs:110:11-20
        (Num a0) arising from the literal ‘1’ at src/NQueens.hs:110:20
    • In a stmt of a 'do' block: num <- mkIntNum 1
      In the expression:
        do sort <- mkIntSort
           one <- mkInt 1 sort
           zero <- mkZero x
           first1 <- mkEq x (zero)
           ....
      In an equation for ‘onceInARow’:
          onceInARow x
            = do sort <- mkIntSort
                 one <- mkInt 1 sort
                 zero <- mkZero x
                 ....
    |
110 |    num <- mkIntNum 1
    |           ^^^^^^^^^^

/home/vyacheslav/mlcs-2021-z3-assignment-tamarinvs19/src/NQueens.hs:125:4: warning: [-Wname-shadowing]
    This binding for ‘sum’ shadows the existing binding
      imported from ‘Prelude’ at src/NQueens.hs:1:8-14
      (and originally defined in ‘Data.Foldable’)
    |
125 |    sum <- sumBv xs
    |    ^^^

/home/vyacheslav/mlcs-2021-z3-assignment-tamarinvs19/src/NQueens.hs:150:4: warning: [-Wunused-matches]
    Defined but not used: ‘addedLeft’
    |
150 |    addedLeft <- sequenceA $ map (\(ast, zer) -> mkConcat zer ast) (zipWith (,) xs zeros)
    |    ^^^^^^^^^
[4 of 4] Compiling Paths_mlcs_class_z3_assignment
Preprocessing test suite 'task-test' for mlcs-class-z3-assignment-0.1..
Building test suite 'task-test' for mlcs-class-z3-assignment-0.1..
[2 of 2] Compiling Main
Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-3.0.1.0/build/task-test/task-test ...
Preprocessing executable 'problems' for mlcs-class-z3-assignment-0.1..
Building executable 'problems' for mlcs-class-z3-assignment-0.1..
[1 of 2] Compiling Main [Optimisation flags changed]
[2 of 2] Compiling Paths_mlcs_class_z3_assignment
Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-3.0.1.0/build/problems/problems ...

mlcs-class-z3-assignment> copy/register
Installing library in /home/vyacheslav/mlcs-2021-z3-assignment-tamarinvs19/.stack-work/install/x86_64-linux-tinfo6/34ac4eaf140487c5c0864f95c8c3b13a9f560baba7322eff2edbe83e22dd40d4/8.8.4/lib/x86_64-linux-ghc-8.8.4/mlcs-class-z3-assignment-0.1-7W652HBnELx9D0qXjlmn5T
Installing executable problems in /home/vyacheslav/mlcs-2021-z3-assignment-tamarinvs19/.stack-work/install/x86_64-linux-tinfo6/34ac4eaf140487c5c0864f95c8c3b13a9f560baba7322eff2edbe83e22dd40d4/8.8.4/bin
Registering library for mlcs-class-z3-assignment-0.1..
mlcs-class-z3-assignment> test (suite: task-test)

Progress 1/2: mlcs-class-z3-assignmenttask-test: Z3 error: Sort mismatch at argument #1 for function (declare-fun - (Int Int) Int) supplied sort is (_ BitVec 1)

mlcs-class-z3-assignment> Test suite task-test failed
Completed 2 action(s).
Test suite failure for package mlcs-class-z3-assignment-0.1
    task-test:  exited with: ExitFailure 1
Logs printed to console