From 844f81f5b592936dc0b03adac52f2a54eecc03bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Wed, 5 Feb 2020 18:50:48 +0100
Subject: [PATCH] Count program and integer variable IDs separately

---
 src/translate/verify_properties.rs         |  3 ++-
 src/translate/verify_properties/context.rs | 18 +++++++++++++++---
 2 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index 1aac8e3..aef8de3 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -163,7 +163,8 @@ where
 		.map(|x| (std::rc::Rc::clone(x), completed_definition(x)));
 
 	// Earlier log messages may have assigned IDs to the variable declarations, so reset them
-	context.variable_declaration_ids.borrow_mut().clear();
+	context.program_variable_declaration_ids.borrow_mut().clear();
+	context.integer_variable_declaration_ids.borrow_mut().clear();
 
 	let print_title = |title, section_separator|
 	{
diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs
index 9db2c6f..a1678ed 100644
--- a/src/translate/verify_properties/context.rs
+++ b/src/translate/verify_properties/context.rs
@@ -26,7 +26,8 @@ pub(crate) struct Context
 	pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
 	pub variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
 	pub variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>,
-	pub variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
+	pub program_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
+	pub integer_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
 }
 
 impl Context
@@ -49,7 +50,10 @@ impl Context
 				std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
 			variable_declaration_domains:
 				std::cell::RefCell::new(VariableDeclarationDomains::new()),
-			variable_declaration_ids: std::cell::RefCell::new(VariableDeclarationIDs::new()),
+			program_variable_declaration_ids:
+				std::cell::RefCell::new(VariableDeclarationIDs::new()),
+			integer_variable_declaration_ids:
+				std::cell::RefCell::new(VariableDeclarationIDs::new()),
 		}
 	}
 }
@@ -181,7 +185,15 @@ impl crate::traits::VariableDeclarationID for Context
 		variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
 		-> usize
 	{
-		let mut variable_declaration_ids = self.variable_declaration_ids.borrow_mut();
+		use crate::traits::VariableDeclarationDomain;
+
+		let mut variable_declaration_ids = match self.variable_declaration_domain(
+			variable_declaration)
+		{
+			Some(crate::Domain::Program) => self.program_variable_declaration_ids.borrow_mut(),
+			Some(crate::Domain::Integer) => self.integer_variable_declaration_ids.borrow_mut(),
+			None => panic!("all variables should be declared at this point"),
+		};
 
 		match variable_declaration_ids.get(variable_declaration)
 		{