CVC 3/4 support broken in tests

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-1405
• Submitted on: 2014-02-05 by (at)rbubel
• Updated: 2014-11-05

Description

The SMT tests for cvc3 abort with

.java.lang.RuntimeException: Error while executing CVC: *** Error while processing a command line option: at de.uka.ilkd.key.smt.SolverType$3.messageIncoming(SolverType.java:501) at de.uka.ilkd.key.smt.Pipe$Receiver.deliverMessage(Pipe.java:224) at de.uka.ilkd.key.smt.Pipe$Receiver.doWork(Pipe.java:208) at de.uka.ilkd.key.smt.Pipe$Worker.run(Pipe.java:103)

that is also the reason why the Hudson builds took 7 hours.

Files

Notes

(at)rbubel at 2014-02-05

CVC Version: 2.4.1

(at)grahl at 2014-02-05

The command line parameters for version 2.4.1 use a different schema as for older versions. The implementation in key.smt.SolverType should make this distinction.

Parameters for 2.4.1 should be: -lang smt -interactive ... for older versions: +lang smt +model +int

(at)grahl at 2014-07-01

Fixed #1349, but test cases still fail...

(at)grahl at 2014-07-01

... but they run through on my local machine.

(at)grahl at 2014-07-28

Same for CVC4.

Invoking the solver from a proof works just fine, but test cases run forever.

History

• (at)rbubel -- (NEW_BUG) 2014-02-05

• (at)rbubel -- (BUGNOTE_ADDED) 2014-02-05

• (at)grahl -- (BUGNOTE_ADDED) 2014-02-05

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2014-02-05

• (at)grahl -- (BUG_DEL_RELATIONSHIP) 2014-07-01

• (at)grahl -- (BUGNOTE_ADDED) 2014-07-01

• (at)grahl -- (BUGNOTE_ADDED) 2014-07-01

• (at)grahl -- (BUGNOTE_ADDED) 2014-07-28

• (at)grahl -- (NORMAL_TYPE) 2014-07-28

• (at)grahl -- (NORMAL_TYPE) 2014-07-28

• (at)grahl -- (NORMAL_TYPE) 2014-10-06

• (at)grahl -- (NORMAL_TYPE) 2014-11-05

Attributes

• Category: SMT
• Status: NEW
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: 86b43f5f2683a4de85cb9eab0f05290243332adb
• Build:
• Tags []
• Labels: ~SMT ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:39:17.975Z
• updated_at: 2017-05-29T02:39:18.302Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0

[WolframPfeifer]

This is no longer relevant.