search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

std::bad_alloc when running a SAT instance with --print-witness #54

Closed rodrigo7491 closed 9 months ago

rodrigo7491 commented 9 months ago

When running chc-LIA_177 from CHC-COMP 2023, Golem outputs the following:

For the command golem chc-LIA_177.smt2 the output is sat.

For the command golem --print-witness chc-LIA_177.smt2 the output is as below.

sat
terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
Aborted (core dumped)
rodrigo7491 commented 9 months ago

For some other instances, e.g., chc-LIA_131, golem gives this error but produces a (partial?) model.

Output for golem --print-witness chc-LIA_131.smt2:

sat
  (define-fun MAIN ((|x#247| Int) (|x#248| Int) (|x#249| Bool) (|x#250| Bool) (|x#251| Bool) (|x#252| Int) (|x#253| Int) (|x#254| Int) (|x#255| Bool) (|x#256| Int) (|x#257| Bool) (|x#258| Bool) (|x#259| Bool) (|x#260| Int) (|x#261| Bool) (|x#262| Bool) (|x#263| Bool) (|x#264| Bool) (|x#265| Bool) (|x#266| Bool) (|x#267| Bool) (|x#268| Bool) (|x#269| Bool) (|x#270| Bool)) Bool
    (and (not |x#258|) (not |x#262|) (not |x#265|) (not |x#268|) (not |x#269|) |x#270| (and (not |x#249|) (<= 0 (+ |x#247| (* (- 1) |x#248|) (* (- 1) |x#253|) |x#254|))) (or (not |x#267|) (<= 1 (+ (* (- 1) |x#252|) |x#253|))) (or |x#255| (not |x#264|)) (or |x#259| (not |x#267|)) (or (not |x#259|) (not |x#266|) (<= 10 (+ (* (- 1) |x#252|) |x#253|))) (or...
...
...
...
...)))))))))))))))))))))))))))))))))))))))))))))terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
Aborted (core dumped)