search

c-cube / sidekick

A modular library for CDCL(T) SMT solvers, with [wip] proof generation.
https://c-cube.github.io/sidekick/
Apache License 2.0
24 stars 15 forks source link

Bug with smt2 #19

Closed ar7-612 closed 1 year ago

ar7-612 commented 1 year ago

Version

Tested on commit 40a743badb70f29ca47007eb4e394afdf1ff006d

Reproduce

Command

sidekick file.smt2

File.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :status sat)

(declare-fun A () Real)
(declare-fun B () Real)
(declare-fun C () Real)

(assert (or (= B C) (not (= A B))))

(check-sat)
(exit)

Switching the definition of B with A or C does not provoke this bug

Result

Fatal error: exception File "src/smt/solver.ml", line 213, characters 18-24: Assertion failed

Expected result

sat

c-cube commented 1 year ago

thank you for the report. It lead me to a bit of a rabbit hole, possibly fixing a long standing bug that I thought was in theory combination, but turns out to potentially have been a LRA thing! I'm working on the branch bug-lra-minimized if you want to give it a try.

ar7-612 commented 1 year ago

Glad if it helps ! For information, I’m currently using Sidekick for my internship. The goal is to implement a theory of partial order (only comparison between variable) and compare it to a more generic theory (i.e. LRA). Found this issue while trying to compare my theory to LRA.

PS : I think the two lines change of 8fbf482 in wip-19 should also be changed in the main ?

c-cube commented 1 year ago

you're right, wip-19 was not merged yet. I'm worried about a perf regression but it seems fine after running most of the benchmarks I have locally.

I'd be interested in hearing more about your project! Email me if you're game to chat :)