From b28b858f08f0a09b12e8607dfd7c0c4b038c9e0b Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <44122567+bruggerl@users.noreply.github.com>
Date: Wed, 24 Jul 2024 12:16:32 +0200
Subject: [PATCH] Make assume impure (#779)

---
 .../typing/ghost/GhostStmtTyping.scala        |  2 +-
 .../features/assume/assume-simple-01.gobra    | 22 +++++++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 src/test/resources/regressions/features/assume/assume-simple-01.gobra

diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala
index be6569263..922729f74 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala
+++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostStmtTyping.scala
@@ -19,7 +19,7 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl =>
     case PAssert(exp) => assignableToSpec(exp)
     case PRefute(exp) => assignableToSpec(exp)
     case PExhale(exp) => assignableToSpec(exp)
-    case PAssume(exp) => assignableToSpec(exp) ++ isPureExpr(exp)
+    case PAssume(exp) => assignableToSpec(exp)
     case PInhale(exp) => assignableToSpec(exp)
     case PFold(acc) => wellDefFoldable(acc)
     case PUnfold(acc) => wellDefFoldable(acc)
diff --git a/src/test/resources/regressions/features/assume/assume-simple-01.gobra b/src/test/resources/regressions/features/assume/assume-simple-01.gobra
new file mode 100644
index 000000000..3181e40a4
--- /dev/null
+++ b/src/test/resources/regressions/features/assume/assume-simple-01.gobra
@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package assumption
+
+type person struct {
+	name string
+	age  int
+}
+
+func f() {
+	p := &person{name: "Pereira", age: 12}
+	assume acc(p) // impure assume does not lead to contradiction
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert false
+}
+
+func g() {
+	p := &person{name: "Pereira", age: 12}
+	inhale acc(p) // inhale leads to contradiction
+	assert false
+}
\ No newline at end of file