Skip to content

Wrong bitwuzla answer for QF_UF #465

@filipeom

Description

@filipeom

Raised in #450

cc @remigerme

(set-info :status unsat)
(set-logic ALL)
(declare-fun f (Bool) Bool)
(assert
 (f false))
(assert
 (let (($x10 (f false)))
(not $x10)))
(check-sat)
$ dune exec -- smtml run --solver z3 test.smt2
unsat                                  
$ dune exec -- smtml run --solver bitwuzla test.smt2
sat                                    
smtml: internal error, uncaught exception:
       Failure("Expected status: unsat, but solver returned sat")
       Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
       Called from Fmt.failwith in file "src/fmt.ml" (inlined), line 25, characters 19-36
       Called from Smtml__Interpret.Make.eval in file "src/smtml/interpret.ml", line 44, characters 13-75
       Called from Smtml__Interpret.Make.loop in file "src/smtml/interpret.ml", line 84, characters 11-61
       Called from Dune__exe__Cmd_run.run.run_file.(fun) in file "src/bin/cmd_run.ml", line 54, characters 21-67
       Called from Stdlib__Fun.protect in file "fun.ml", line 34, characters 8-15
       Re-raised at Stdlib__Fun.protect in file "fun.ml", line 39, characters 6-52
       Called from Stdlib__List.fold_left in file "list.ml", line 125, characters 24-34
       Called from Dune__exe__Cmd_run.run in file "src/bin/cmd_run.ml", line 87, characters 14-52
       Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
       Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions