Skip to content

Commit a7a3a1e

Browse files
Fix broken validate mode tests
1 parent e33fe25 commit a7a3a1e

7 files changed

Lines changed: 8 additions & 19 deletions

File tree

vehicle/src/Vehicle/Backend/Queries/UserVariableElimination/VariableReconstruction.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ createInitialAssignment ::
5353
QueryVariableAssignment ->
5454
MixedVariableAssignment
5555
createInitialAssignment queryVariableMap (QueryVariableAssignment valuesByQueryVar) = do
56-
let missingVariable var = developerError ("Missing query variable" <+> pretty var)
56+
let missingVariable var = developerError ("Solver returned additional unknown variable" <+> pretty var)
5757
let mapQueryVariable var = coerce $ fromMaybe (missingVariable var) (Map.lookup var queryVariableMap)
5858
let valuesByNetworkVar = ZeroDimTensor <$> Map.mapKeys mapQueryVariable valuesByQueryVar
5959
valuesByNetworkVar
Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +0,0 @@
1-
Something went wrong internally. Please report the error shown below to `https://github.com/vehicle-lang/vehicle/issues`.
2-
Error: Missing query variable f_X[1]
3-
Stack:
4-
CallStack (from HasCallStack):
5-
developerError, called at src/Vehicle/Backend/Queries/UserVariableElimination/VariableReconstruction.hs:56:29 in vehicle-0.16.1-inplace:Vehicle.Backend.Queries.UserVariableElimination.VariableReconstruction
Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +0,0 @@
1-
Something went wrong internally. Please report the error shown below to `https://github.com/vehicle-lang/vehicle/issues`.
2-
Error: Missing query variable f_X[1]
3-
Stack:
4-
CallStack (from HasCallStack):
5-
developerError, called at src/Vehicle/Backend/Queries/UserVariableElimination/VariableReconstruction.hs:56:29 in vehicle-0.16.1-inplace:Vehicle.Backend.Queries.UserVariableElimination.VariableReconstruction

vehicle/tests/golden/validate/error/test.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
[
22
{
33
"name": "missingNetwork",
4-
"run": "vehicle verify -s spec.vcl -v TestVerifier --network f:fake.onnx --property trivial --verifier-location=testVerifier --verifier-args='sat 'f_X[0]=0.2,f_X[1]=0.3,f_Y[0]=3.0'' --cache verify-cache > /dev/null ; mv fake.onnx fake-changed.onnx && vehicle validate -c verify-cache -j && mv fake-changed.onnx fake.onnx",
4+
"run": "vehicle verify -s spec.vcl -v TestVerifier --network f:fake.onnx --property trivial --verifier-location=testVerifier --verifier-args='sat 'f_X[0]=0.2,f_Y[0]=3.0'' --cache verify-cache > /dev/null ; mv fake.onnx fake-changed.onnx && vehicle validate -c verify-cache -j && mv fake-changed.onnx fake.onnx",
55
"needs": ["fake.onnx", "spec.vcl", "../../../testVerifier"],
66
"external": ["TestVerifier"],
77
"ignore": {
@@ -14,7 +14,7 @@
1414
},
1515
{
1616
"name": "alteredNetwork",
17-
"run": "vehicle verify -s spec.vcl -v TestVerifier --network f:fake.onnx --property trivial --verifier-location=testVerifier --verifier-args='sat 'f_X[0]=0.2,f_X[1]=0.3,f_Y[0]=3.0'' --cache verify-cache > /dev/null ; echo \"FAKE CHANGED ONNX NETWORK\" > fake.onnx && vehicle validate -c verify-cache -j && echo \"FAKE ONNX NETWORK\n\" > fake.onnx",
17+
"run": "vehicle verify -s spec.vcl -v TestVerifier --network f:fake.onnx --property trivial --verifier-location=testVerifier --verifier-args='sat 'f_X[0]=0.2,f_Y[0]=3.0'' --cache verify-cache > /dev/null ; echo \"FAKE CHANGED ONNX NETWORK\" > fake.onnx && vehicle validate -c verify-cache -j && echo \"FAKE ONNX NETWORK\n\" > fake.onnx",
1818
"needs": ["fake.onnx", "spec.vcl", "../../../testVerifier"],
1919
"external": ["TestVerifier"],
2020
"ignore": {

vehicle/tests/golden/validate/success/simple.err.golden

Lines changed: 0 additions & 5 deletions
This file was deleted.

vehicle/tests/golden/validate/success/simple.out.golden

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,7 @@
1+
Verifying properties:
2+
trivial [........................................................] 0/1 queries trivial [========================================================] 1/1 queries
3+
result: 🗸 - TestVerifier found a witness
4+
15
{
26
"tag": "Verified"
37
}

vehicle/tests/golden/validate/success/test.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
[
22
{
33
"name": "simple",
4-
"run": "vehicle verify -s spec.vcl -v TestVerifier --network f:fake.onnx --property trivial --verifier-location=testVerifier --verifier-args='sat 'f_X[0]=0.2,f_X[1]=0.3,f_Y[0]=3.0'' --cache verify-cache > /dev/null ; vehicle validate -c verify-cache -j",
4+
"run": "vehicle verify -s spec.vcl -v TestVerifier --network f:fake.onnx --property trivial --verifier-location=testVerifier --verifier-args='sat 'f_X[0]=0,f_Y[0]=3.0'' --cache verify-cache ; vehicle validate -c verify-cache -j",
55
"needs": ["fake.onnx", "spec.vcl", "../../../testVerifier"],
66
"external": ["TestVerifier"],
77
"ignore": {

0 commit comments

Comments
 (0)