[Question][Hw2] "Conversion failed" Error for printing Sudoku Board

[Gimongjin]

In the Sudoku Solver, I implemented all the codes that I need. But when I run the test case ./sudoku test/sudoku1.scm, I have the result like below:

satisfiable Fatal error: exception Z3.Error("Conversion failed.") But when I inserted the line Z3.Solver.to_string solver |> print_endline; in the solver function, I have the result

... (not (= x63 x85)) (not (= x63 8)) (not (= x63 x83)) (not (= x63 9)) (not (= x63 1)) (not (= x63 4)) (not (= x63 x65)) (not (= x63 x64)) (not (= 7 9)) (not (= x86 9)) (not (= x86 7)) (not (= 5 9)) (not (= 5 7)) (not (= 5 x86)) (not (= x77 9)) (not (= x77 7)) (not (= x77 x86)) (not (= x77 5)) (not (= x76 9)) (not (= x76 7)) (not (= x76 x86)) (not (= x76 5)) (not (= x76 x77)) (not (= x68 9)) (not (= x68 7)) (not (= x68 x86)) (not (= x68 5)) (not (= x68 x77)) (not (= x68 x76)) (not (= 8 9)) (not (= 8 7)) (not (= 8 x86)) (not (= 8 5)) (not (= 8 x77)) (not (= 8 x76)) (not (= 8 x68)) (not (= 2 9)) (not (= 2 7)) (not (= 2 x86)) (not (= 2 5)) (not (= 2 x77)) (not (= 2 x76)) (not (= 2 x68)) (not (= 2 8)))) (model-add x71 () Int 8) (model-add x11 () Int 7) (model-add x85 () Int 6) (model-add x23 () Int 3) (model-add x55 () Int 4) (model-add x76 () Int 6) (model-add x63 () Int 5) (model-add x16 () Int 3) (model-add x26 () Int 5) (model-add x53 () Int 9) (model-add x41 () Int 2) (model-add x56 () Int 8) (model-add x62 () Int 1) (model-add x65 () Int 7) (model-add x33 () Int 7) (model-add x35 () Int 1) (model-add x57 () Int 5) (model-add x46 () Int 7) (model-add x24 () Int 4) (model-add x31 () Int 5) (model-add x86 () Int 1) (model-add x72 () Int 7) (model-add x03 () Int 6) (model-add x51 () Int 1) (model-add x83 () Int 2) (model-add x18 () Int 8) (model-add x52 () Int 3) (model-add x20 () Int 1) (model-add x25 () Int 2) (model-add x37 () Int 2) (model-add x32 () Int 9) (model-add x44 () Int 5) (model-add x05 () Int 8) (model-add x77 () Int 3) (model-add x81 () Int 4) (model-add x82 () Int 5) (model-add x42 () Int 6) (model-add x64 () Int 3) (model-add x70 () Int 2) (model-add x36 () Int 4) (model-add x02 () Int 4) (model-add x12 () Int 2) (model-add x47 () Int 9) (model-add x60 () Int 9) (model-add x17 () Int 4) (model-add x68 () Int 4) (model-add x28 () Int 7) (model-add x80 () Int 3) (model-add x08 () Int 2) (model-add x06 () Int 9) (model-add x07 () Int 1) ...

Which coincides with the solution of the Sudoku. If the Sudoku is unsatisfiable, the result has no problem since it does not have to print any Sudoku board. I cannot find out why this kind of problem occurs. Is it a problem from my code? I think my code gives a proper FOL formula to represent the Sudoku, and I think solver is finding the right solution - but it has a trouble in just printing the solution.

Thank you.

[Hhro]

Hi.

Based on the Z3 code, I guess the exception occurs at this line. Maybe the value of the board in your model doesn't have an integer numeric sort. Please recheck it.

Thanks.

[Allgot]

In my case, I didn't use provided mk_variable function for some numbers and that caused 'conversion failed' exception. So I think checking that again will be very helpful for this :)

[kohs100]

You should assign variable (w/ mk_variable) for every slots in sudoku even if there is already non-zero number at given input...

[Gimongjin]

I solved the problem. Thanks a lot to everyone.