c-cube / sidekick Goto Github PK

./sidekick tests/unsat/data_acycl_if.smt2 --bt -d 50

could be in msat or in a bad conflict

replace preprocess_lit by preprocess_term, and hook that up into the CC itself. This is necessary when other theories produce new terms that contain boolean connectives.

A call to simple.solve seems to take an arbitrary amount of time in tracing. Spends its time doing pivots. It might be a problem with epsilons?

repro:

$ /sidekick.sh --stat tests/unsat/pb_real_30_0600_10_18.smt2 -p

http://fmv.jku.at/cnfuzzdd/

an array.sort/bigarray.sort (perhaps functorized) that works in-place on slices would be super useful as we use sort a lot in the SAT solver.

Version

Tested on commit 40a743b

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

[31;1mError�[0m: internal error: at file '/home/simon/w/sidekick/tests/QF_UF/20170829-Rodin/smt834303034702425531.smt2': line 15, col 0 to line 16, col 22:
unsupported term (! circuit :named hyp1)

on QF_UF/20170829-Rodin/smt834303034702425531.smt2