From 383ca601efc51854e0b49c545373bd453c1983d0 Mon Sep 17 00:00:00 2001 From: Elizabeth Polgreen Date: Thu, 9 May 2024 14:46:31 +0100 Subject: [PATCH] add test for instance procedure call bug --- src/test/scala/SMTLIB2Spec.scala | 3 +++ src/test/scala/VerifierSpec.scala | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala index 502fba632..f2437cca4 100644 --- a/src/test/scala/SMTLIB2Spec.scala +++ b/src/test/scala/SMTLIB2Spec.scala @@ -439,6 +439,9 @@ class SMTLIB2Spec extends AnyFlatSpec { "test-instance-procedure-call-7.ucl" should "verify all assertions." in { SMTLIB2Spec.expectedFails("./test/test-instance-procedure-call-7.ucl", 0) } + "test-instance-procedure-calls-1.ucl" should "verify all assertions." in { + VerifierSpec.expectedFails("./test/test-instance-procedure-call-0.ucl", 0) + } "sp-basic.ucl" should "verify all assertions." in { SMTLIB2Spec.expectedFails("./test/sp-basic.ucl", 0) } diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala index bf698bac1..40b410027 100644 --- a/src/test/scala/VerifierSpec.scala +++ b/src/test/scala/VerifierSpec.scala @@ -556,6 +556,9 @@ class ModuleVerifSpec extends AnyFlatSpec { "test-instance-procedure-call-7.ucl" should "verify all assertions." in { VerifierSpec.expectedFails("./test/test-instance-procedure-call-7.ucl", 0) } + "test-instance-procedure-calls-1.ucl" should "verify all assertions." in { + VerifierSpec.expectedFails("./test/test-instance-procedure-call-0.ucl", 0) + } "sp-basic.ucl" should "verify all assertions." in { VerifierSpec.expectedFails("./test/sp-basic.ucl", 0) }