Runtime error occurs when handling property "G true"
Using property
(G true)
for the ABS example for the ICTSS 2023 paper (https://bitbucket.org/JanPeleska/ifip_ictss_2023/src/6d0576e/), I obtain the following error upon running the test harness as
./testharness faultDomainAbs.txt prop.txt -seed=2
[...]
Creating monitor for formula '(G true)'
Determinining implication relationships
terminate called after throwing an instance of 'std::runtime_error'
what(): Solver returned neither `sat` nor `unsat`.
Solver output: (error "line 21629 column 17: invalid function application, arguments missing")
Referring to this problem: (declare-fun vehicleReferenceVelocity () Real)
(declare-fun brakePressureFromDriver () Real)
(declare-fun wheelVelocity () Real)
(declare-fun yaw () Real)
(declare-fun a () Real)
(declare-fun steeringAngle () Real)
(declare-fun brakePressureInValve () Bool)
(declare-fun brakePressureOutValve () Bool)
(declare-fun brakePumpStatus () Int)
(declare-fun A_MINUS () Real)
(declare-fun A_MINUS_GMA () Real)
(declare-fun A_PLUS () Real)
(declare-fun BIG_A_PLUS () Real)
(declare-fun MAX_BRAKE_SLIP () Real)
(declare-fun OPEN () Bool)
(declare-fun CLOSED () Bool)
(declare-fun ON () Int)
(declare-fun OFF () Int)
(declare-fun SLOW_ON () Int)
(declare-fun YAW_THRESHOLD () Real)
(declare-fun STEERING_ANGLE_THRESHOLD () Real)
(declare-fun slip () Real)
(assert (and (and) (and (<= wheelVelocity 230) (>= vehicleReferenceVelocity 0) (= A_MINUS -0.02644) (= A_MINUS_GMA -0.01322) (= A_PLUS 0.01193) (= BIG_A_PLUS 0.01653) (= MAX_BRAKE_SLIP -0.3) (= YAW_THRESHOLD 5.0) (= STEERING_ANGLE_THRESHOLD 5.0) (= OPEN true) (= CLOSED false) (= ON 1) (= OFF 0) (= SLOW_ON 2) (>= wheelVelocity 0) (<= vehicleReferenceVelocity 230) (>= brakePressureFromDriver 0) (<= brakePressureFromDriver 1) (= slip (ite (= vehicleReferenceVelocity 0) 0 (/ (- wheelVelocity vehicleReferenceVelocity) vehicleReferenceVelocity))) (<= a 0.02) (>= a (- 0.03)) (>= yaw -90.0) (<= yaw 90.0) (>= steeringAngle -90.0) (<= steeringAngle 90.0))))
(check-sat)
Note that the generated formula contains conjunction (and)
without arguments.