diff --git a/build.gradle.kts b/build.gradle.kts
index 282a38fe25..922c1084ea 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "3.0.0"
+    version = "3.0.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/subprojects/cfa/cfa-analysis/src/test/resources/counter_fp_true.cfa b/subprojects/cfa/cfa-analysis/src/test/resources/counter_fp_true.cfa
index bb8b90ba84..242ef6d09c 100644
--- a/subprojects/cfa/cfa-analysis/src/test/resources/counter_fp_true.cfa
+++ b/subprojects/cfa/cfa-analysis/src/test/resources/counter_fp_true.cfa
@@ -1,5 +1,5 @@
 main process cfa {
-	var x : fp[8:24]
+	var x : fp[8,24]
 
 	init loc L0
     loc L1
diff --git a/subprojects/cfa/cfa-analysis/src/test/resources/fp1.cfa b/subprojects/cfa/cfa-analysis/src/test/resources/fp1.cfa
index ee192546d0..b148f0a59d 100644
--- a/subprojects/cfa/cfa-analysis/src/test/resources/fp1.cfa
+++ b/subprojects/cfa/cfa-analysis/src/test/resources/fp1.cfa
@@ -1,7 +1,7 @@
 main process cfa {
-	var f2 : fp[5:11]
-	var f3 : fp[11:53]
-	var f4 : fp[11:53]
+	var f2 : fp[5,11]
+	var f3 : fp[11,53]
+	var f4 : fp[11,53]
 	var b1 : bv[4]
 
     init loc L1
@@ -13,9 +13,9 @@ main process cfa {
     error loc ERR
 
     L1 -> L2 { f2 := 5'b10010.10'd0 }
-    L2 -> L3 { f3 := fptofp[11:53][RNE] f2 }
+    L2 -> L3 { f3 := fptofp[11,53][RNE] f2 }
     L3 -> L4 { b1 := 4'd8 }
-    L4 -> L5 { f4 := fpfrombv[11:53][u][RNE] b1 }
+    L4 -> L5 { f4 := fpfrombv[11,53][u][RNE] b1 }
     L5 -> END { assume f3 = f4 }
     L5 -> ERR { assume not (f3 = f4) }
 }
\ No newline at end of file
diff --git a/subprojects/cfa/cfa-analysis/src/test/resources/fp2.cfa b/subprojects/cfa/cfa-analysis/src/test/resources/fp2.cfa
index 27a6d8b8b7..5c827e9a31 100644
--- a/subprojects/cfa/cfa-analysis/src/test/resources/fp2.cfa
+++ b/subprojects/cfa/cfa-analysis/src/test/resources/fp2.cfa
@@ -1,8 +1,8 @@
 main process cfa {
-	var f2 : fp[2:3]
-	var f3 : fp[2:3]
-	var f4 : fp[2:3]
-	var f5 : fp[2:3]
+	var f2 : fp[2,3]
+	var f3 : fp[2,3]
+	var f4 : fp[2,3]
+	var f5 : fp[2,3]
 
     init loc L1
     loc L2
diff --git a/subprojects/cfa/cfa/src/main/antlr/CfaDsl.g4 b/subprojects/cfa/cfa/src/main/antlr/CfaDsl.g4
index 29bb06c56a..dccc21ea60 100644
--- a/subprojects/cfa/cfa/src/main/antlr/CfaDsl.g4
+++ b/subprojects/cfa/cfa/src/main/antlr/CfaDsl.g4
@@ -604,7 +604,7 @@ SIGNEDNESS
     ;
 
 FP_TYPE_DECL
-    :   LBRACK NAT COLON NAT RBRACK
+    :   LBRACK NAT COMMA NAT RBRACK
     ;
 
 FP_ROUNDINGMODE
diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java
index e7e53b4c5f..f5744f4935 100644
--- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java
+++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java
@@ -875,7 +875,7 @@ private int getBvSize(String text) {
 		}
 
 		private int getExp(String text) {
-			Pattern pattern = Pattern.compile("\\[([0-9]*):([0-9]*)]");
+			Pattern pattern = Pattern.compile("\\[([0-9]*),([0-9]*)]");
 			Matcher matcher = pattern.matcher(text);
 			if (matcher.find())
 			{
@@ -884,7 +884,7 @@ private int getExp(String text) {
 		}
 
 		private int getSignificand(String text) {
-			Pattern pattern = Pattern.compile("\\[([0-9]*):([0-9]*)]");
+			Pattern pattern = Pattern.compile("\\[([0-9]*),([0-9]*)]");
 			Matcher matcher = pattern.matcher(text);
 			if (matcher.find())
 			{
diff --git a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaType.java b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaType.java
index faaf33e2f2..51ca69ccc2 100644
--- a/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaType.java
+++ b/subprojects/cfa/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaType.java
@@ -95,7 +95,7 @@ public Type visitFpType(FpTypeContext ctx) {
 		}
 
 		private int getExp(String text) {
-			Pattern pattern = Pattern.compile("\\[([0-9]*):([0-9]*)]");
+			Pattern pattern = Pattern.compile("\\[([0-9]*),([0-9]*)]");
 			Matcher matcher = pattern.matcher(text);
 			if (matcher.find())
 			{
@@ -104,7 +104,7 @@ private int getExp(String text) {
 		}
 
 		private int getSignificand(String text) {
-			Pattern pattern = Pattern.compile("\\[([0-9]*):([0-9]*)]");
+			Pattern pattern = Pattern.compile("\\[([0-9]*),([0-9]*)]");
 			Matcher matcher = pattern.matcher(text);
 			if (matcher.find())
 			{
diff --git a/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/dsl/CfaDslManagerTest.java b/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/dsl/CfaDslManagerTest.java
index 58dc74c495..d88bd72176 100644
--- a/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/dsl/CfaDslManagerTest.java
+++ b/subprojects/cfa/cfa/src/test/java/hu/bme/mit/theta/cfa/dsl/CfaDslManagerTest.java
@@ -57,8 +57,15 @@ public static Collection<Object[]> data() {
 
 				{"/bv.cfa", 1, 6, 6, 6},
 
-				{"/bv2.cfa", 1, 6, 6, 6}
+				{"/bv2.cfa", 1, 6, 6, 6},
 
+				{"/bv3.cfa", 1, 6, 6, 6},
+
+				{"/bv4.cfa", 2, 7, 8, 8},
+
+				{"/fp1.cfa", 4, 7, 6, 6},
+
+				{"/fp2.cfa", 4, 7, 6, 6}
 		});
 	}
 
diff --git a/subprojects/cfa/cfa/src/test/resources/fp1.cfa b/subprojects/cfa/cfa/src/test/resources/fp1.cfa
index ee192546d0..b148f0a59d 100644
--- a/subprojects/cfa/cfa/src/test/resources/fp1.cfa
+++ b/subprojects/cfa/cfa/src/test/resources/fp1.cfa
@@ -1,7 +1,7 @@
 main process cfa {
-	var f2 : fp[5:11]
-	var f3 : fp[11:53]
-	var f4 : fp[11:53]
+	var f2 : fp[5,11]
+	var f3 : fp[11,53]
+	var f4 : fp[11,53]
 	var b1 : bv[4]
 
     init loc L1
@@ -13,9 +13,9 @@ main process cfa {
     error loc ERR
 
     L1 -> L2 { f2 := 5'b10010.10'd0 }
-    L2 -> L3 { f3 := fptofp[11:53][RNE] f2 }
+    L2 -> L3 { f3 := fptofp[11,53][RNE] f2 }
     L3 -> L4 { b1 := 4'd8 }
-    L4 -> L5 { f4 := fpfrombv[11:53][u][RNE] b1 }
+    L4 -> L5 { f4 := fpfrombv[11,53][u][RNE] b1 }
     L5 -> END { assume f3 = f4 }
     L5 -> ERR { assume not (f3 = f4) }
 }
\ No newline at end of file
diff --git a/subprojects/cfa/cfa/src/test/resources/fp2.cfa b/subprojects/cfa/cfa/src/test/resources/fp2.cfa
index 27a6d8b8b7..5c827e9a31 100644
--- a/subprojects/cfa/cfa/src/test/resources/fp2.cfa
+++ b/subprojects/cfa/cfa/src/test/resources/fp2.cfa
@@ -1,8 +1,8 @@
 main process cfa {
-	var f2 : fp[2:3]
-	var f3 : fp[2:3]
-	var f4 : fp[2:3]
-	var f5 : fp[2:3]
+	var f2 : fp[2,3]
+	var f3 : fp[2,3]
+	var f4 : fp[2,3]
+	var f5 : fp[2,3]
 
     init loc L1
     loc L2